gori - brismu bridi

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

Theorem gori 86

Description: Inference form of right side of df-go 83 (Contributed by la korvo, 30-Jul-2023.)

**Hypothesis**
Ref	Expression
gori.0	⊢ ge ganai broda gi brode gi ganai brode gi broda

**Assertion**
Ref	Expression
gori	⊢ go broda gi brode

**Proof of Theorem gori**
Step	Hyp	Ref	Expression
1		gori.0	. 2 ⊢ ge ganai broda gi brode gi ganai brode gi broda
2		df-go 83	. . 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-rei 53	. 2 ⊢ ganai ge ganai broda gi brode gi ganai brode gi broda gi go broda gi brode
4	1, 3	ax-mp 10	1 ⊢ go broda gi brode

Colors of variables: sumti selbri bridi

Syntax hints: ganai bgan 9 ge bge 47 go bgo 82

This theorem was proved from axioms: ax-mp 10 ax-ge-re 49

This theorem depends on definitions: df-go 83

This theorem is referenced by: iso 87