goli - brismu bridi

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

Theorem goli 62

Description: Inference form of left side of df-go 61 (Contributed by la korvo, 29-Jul-2023.)

**Hypothesis**
Ref	Expression
goli.0	⊢ go broda gi brode

**Assertion**
Ref	Expression
goli	⊢ ge ganai broda gi brode gi ganai brode gi broda

**Proof of Theorem goli**
Step	Hyp	Ref	Expression
1		goli.0	. 2 ⊢ go broda gi brode
2		df-go 61	. . 3 ⊢ ge ganai go broda gi brode gi ge ganai broda gi brode gi ganai brode gi broda gi ganai ge ganai broda gi brode gi ganai brode gi broda gi go broda gi brode
3	2	ge-lei 46	. 2 ⊢ ganai go broda gi brode gi ge ganai broda gi brode gi ganai brode gi broda
4	1, 3	ax-mp 10	1 ⊢ ge ganai broda gi brode gi ganai brode gi broda

Colors of variables: sumti selbri bridi

Syntax hints: ganai bgan 9 ge bge 42 go bgo 60

This theorem was proved from axioms: ax-mp 10 ax-ge-le 43

This theorem depends on definitions: df-go 61

This theorem is referenced by: go-ganai 63