brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  ge-dist-ga

---

Theorem ge-dist-ga 174

Description: {ge} distributes over {ga}. (Contributed by la korvo, 14-Jul-2025.)

Assertion

Ref	Expression
ge-dist-ga	⊢ go ge broda gi ga brode gi brodi gi ga ge broda gi brode gi ge broda gi brodi

---

Proof of Theorem ge-dist-ga

Step	Hyp	Ref	Expression
1		ga-lin 165	. . 3 ⊢ ganai ge broda gi brode gi ga ge broda gi brode gi ge broda gi brodi
2		ga-rin 166	. . 3 ⊢ ganai ge broda gi brodi gi ga ge broda gi brode gi ge broda gi brodi
3	1, 2	garidan 169	. 2 ⊢ ganai ge broda gi ga brode gi brodi gi ga ge broda gi brode gi ge broda gi brodi
4		ga-lin 165	. . . 4 ⊢ ganai brode gi ga brode gi brodi
5	4	ge-pairr 81	. . 3 ⊢ ganai ge broda gi brode gi ge broda gi ga brode gi brodi
6		ga-rin 166	. . . 4 ⊢ ganai brodi gi ga brode gi brodi
7	6	ge-pairr 81	. . 3 ⊢ ganai ge broda gi brodi gi ge broda gi ga brode gi brodi
8	5, 7	ga-sum 167	. 2 ⊢ ganai ga ge broda gi brode gi ge broda gi brodi gi ge broda gi ga brode gi brodi
9	3, 8	iso 87	1 ⊢ go ge broda gi ga brode gi brodi gi ga ge broda gi brode gi ge broda gi brodi

Colors of variables: sumti selbri bridi

Syntax hints:   ge bge 47   ga bga 160

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

This theorem depends on definitions:  df-go 83  df-ga 161

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator