brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  ganai-swap12

---

Theorem ganai-swap12 26

Description: Naturally swap the first and second antecedents in an internalized inference. Theorem com12 in [ILE] p. 0. (Contributed by la korvo, 30-Jul-2023.)

Hypothesis

Ref	Expression
ganai-swap12.0	⊢ ganai broda gi ganai brode gi brodi

Assertion

Ref	Expression
ganai-swap12	⊢ ganai brode gi ganai broda gi brodi

---

Proof of Theorem ganai-swap12

Step	Hyp	Ref	Expression
1		id 17	. 2 ⊢ ganai brode gi brode
2		ganai-swap12.0	. 2 ⊢ ganai broda gi ganai brode gi brodi
3	1, 2	syl5com 25	1 ⊢ ganai brode gi ganai broda gi brodi

Colors of variables: sumti selbri bridi

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

This theorem is referenced by:  syl5  27  ge-in-swap12  43  subeq-lem2  354

Copyright terms: Public domain

W3C validator