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

---

Theorem ga-li 148

Description: Deduce a disjunction on the left. (Contributed by la korvo, 4-Jan-2025.)

Hypothesis

Ref	Expression
ga-i.0	⊢ broda

Assertion

Ref	Expression
ga-li	⊢ ga broda gi brode

---

Proof of Theorem ga-li

Step	Hyp	Ref	Expression
1		ga-i.0	. 2 ⊢ broda
2		ga-lin 142	. 2 ⊢ ganai broda gi ga broda gi brode
3	1, 2	ax-mp 10	1 ⊢ ga broda gi brode

Colors of variables: sumti selbri bridi

Syntax hints:  ga bga 137

This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 43

This theorem depends on definitions:  df-go 61  df-ga 138

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator