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

---

Theorem equs4 453

Description: A lemma for substitutions. (Contributed by la korvo, 9-Jul-2025.)

Assertion

Ref	Expression
equs4	⊢ ganai ro da zo'u ganai da du ko'a gi broda gi su'o da zo'u ge da du ko'a gi broda

---

Proof of Theorem equs4

Step	Hyp	Ref	Expression
1		ax-ex 416	. . 3 ⊢ su'o da zo'u da du ko'a
2		foml19.29 429	. . 3 ⊢ ganai ge ro da zo'u ganai da du ko'a gi broda gi su'o da zo'u da du ko'a gi su'o da zo'u ge ganai da du ko'a gi broda gi da du ko'a
3	1, 2	mpan2 74	. 2 ⊢ ganai ro da zo'u ganai da du ko'a gi broda gi su'o da zo'u ge ganai da du ko'a gi broda gi da du ko'a
4		ancl 56	. . . 4 ⊢ ganai ganai da du ko'a gi broda gi ganai da du ko'a gi ge da du ko'a gi broda
5	4	cur 59	. . 3 ⊢ ganai ge ganai da du ko'a gi broda gi da du ko'a gi ge da du ko'a gi broda
6	5	eximi 427	. 2 ⊢ ganai su'o da zo'u ge ganai da du ko'a gi broda gi da du ko'a gi su'o da zo'u ge da du ko'a gi broda
7	3, 6	syl 21	1 ⊢ ganai ro da zo'u ganai da du ko'a gi broda gi su'o da zo'u ge da du ko'a gi broda

Colors of variables: sumti selbri bridi

Syntax hints:   ganai bgan 9   ge bge 47   ro brd 222   du sbdu 250   su'o bsd 414

This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 48  ax-ge-re 49  ax-ge-in 50  ax-gen1 224  ax-spec1 228  ax-qi1 234  ax-ro1-nf 249  ax-ex 416  ax-eb 418  ax-eq 420

This theorem depends on definitions:  df-go 83

This theorem is referenced by:  sub2  454

Copyright terms: Public domain

W3C validator