kii - brismu bridi

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

Theorem kii 13

Description: Inference form of ki 12 (Contributed by la korvo, 27-Jul-2023.)

**Hypotheses**
Ref	Expression
kii.0	⊢ broda
kii.1	⊢ brode

**Assertion**
Ref	Expression
kii	⊢ broda

**Proof of Theorem kii**
Step	Hyp	Ref	Expression
1		kii.1	. 2 ⊢ brode
2		kii.0	. . 3 ⊢ broda
3	2	ki 12	. 2 ⊢ ganai brode gi broda
4	1, 3	ax-mp 10	1 ⊢ broda

Colors of variables: sumti selbri bridi

This theorem was proved from axioms: ax-mp 10 ax-k 11

This theorem is referenced by: (None)