taknii - brismu bridi

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

Theorem taknii 535

Description: Inference form of df-takni 534 (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 534	. 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 101	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 47 cmima sbcmima 319 ckini sbckini 347 ro brdp 463 takni sbtakni 533

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

This theorem depends on definitions: df-go 83 df-takni 534

This theorem is referenced by: (None)