taknii - brismu bridi

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

Theorem taknii 480

Description: Inference form of df-takni 479 (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 479	. 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 ro brd 191 cmima sbcmima 282 ckini sbckini 310 ro brdp 412 takni sbtakni 478

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

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

This theorem is referenced by: (None)