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

---

Theorem kii 14

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)

Copyright terms: Public domain

W3C validator