taknii - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > taknii

Theorem taknii 482

Description: Inference form of df-takni 481 (Contributed by la korvo, 22-Jun-2024.)

**Hypothesis**
Ref	Expression
taknii.0	⊢ ko'a takni ko'e

**Assertion**
Ref	Expression
taknii	⊢ ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai ge da ckini de ko'a gi de ckini di ko'a gi da ckini di ko'a

Distinct variable group: da ,de ,di

**Proof of Theorem taknii**
Step	Hyp	Ref	Expression
1		taknii.0	. 2 ⊢ ko'a takni ko'e
2		df-takni 481	. 2 ⊢ go ko'a takni ko'e gi ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai ge da ckini de ko'a gi de ckini di ko'a gi da ckini di ko'a
3	1, 2	bi 79	1 ⊢ ro da poi ke'a cmima ko'e ku'o zo'u ro de poi ke'a cmima ko'e ku'o zo'u ro di poi ke'a cmima ko'e ku'o zo'u ganai ge da ckini de ko'a gi de ckini di ko'a gi da ckini di ko'a

Colors of variables: sumti selbri bridi

Syntax hints: tsb 1 tss 2 ganai bgan 9 ge bge 42 cmima sbcmima 282 ckini sbckini 310 ro brdp 411 takni sbtakni 480

This theorem was proved from axioms: ax-mp 10 ax-ge-le 43

This theorem depends on definitions: df-go 61 df-takni 481

This theorem is referenced by: (None)