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

---

Theorem ga-dist-ge 182

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

Assertion

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

---

Proof of Theorem ga-dist-ge

Step	Hyp	Ref	Expression
1		ax-ge-le 48	. . . 4 ⊢ ganai ge brode gi brodi gi brode
2	1	ga-pairr 181	. . 3 ⊢ ganai ga broda gi ge brode gi brodi gi ga broda gi brode
3		ax-ge-re 49	. . . 4 ⊢ ganai ge brode gi brodi gi brodi
4	3	ga-pairr 181	. . 3 ⊢ ganai ga broda gi ge brode gi brodi gi ga broda gi brodi
5	2, 4	ge-prod 69	. 2 ⊢ ganai ga broda gi ge brode gi brodi gi ge ga broda gi brode gi ga broda gi brodi
6		ga-lin 165	. . . 4 ⊢ ganai broda gi ga broda gi ge brode gi brodi
7	6	weakal 67	. . 3 ⊢ ganai ge ga broda gi brode gi broda gi ga broda gi ge brode gi brodi
8	6	weakar 63	. . . 4 ⊢ ganai ge broda gi brodi gi ga broda gi ge brode gi brodi
9		ga-rin 166	. . . 4 ⊢ ganai ge brode gi brodi gi ga broda gi ge brode gi brodi
10	8, 9	garian 170	. . 3 ⊢ ganai ge ga broda gi brode gi brodi gi ga broda gi ge brode gi brodi
11	7, 10	garidan 169	. 2 ⊢ ganai ge ga broda gi brode gi ga broda gi brodi gi ga broda gi ge brode gi brodi
12	5, 11	iso 87	1 ⊢ go ga broda gi ge brode gi brodi gi ge ga broda gi brode gi ga 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