taknii - brismu bridi

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

Theorem taknii 541

Description: Inference form of df-takni 540 (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 540	. 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 320 ckini sbckini 348 ro brdp 469 takni sbtakni 539

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

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

This theorem is referenced by: (None)