taknii - brismu bridi

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

Theorem taknii 438

Description: Inference form of df-takni 437 (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 437	. 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 69	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 33 ro brd 177 cmima sbcmima 246 ckini sbckini 273 ro brdp 370 takni sbtakni 436

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

This theorem depends on definitions: df-go 52 df-takni 437

This theorem is referenced by: (None)