foml19.29 - brismu bridi

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

Theorem foml19.29 431

Description: Theorem 19.29 of [Margaris] p. 90. (Contributed by la korvo, 9-Jul-2025.)

**Assertion**
Ref	Expression
foml19.29	⊢ ganai ge ro da zo'u broda gi su'o da zo'u brode gi su'o da zo'u ge broda gi brode

**Proof of Theorem foml19.29**
Step	Hyp	Ref	Expression
1		ax-ge-in 50	. . . 4 ⊢ ganai broda gi ganai brode gi ge broda gi brode
2	1	qi1q 237	. . 3 ⊢ ganai ro da zo'u broda gi ro da zo'u ganai brode gi ge broda gi brode
3		exim 428	. . 3 ⊢ ganai ro da zo'u ganai brode gi ge broda gi brode gi ganai su'o da zo'u brode gi su'o da zo'u ge broda gi brode
4	2, 3	syl 21	. 2 ⊢ ganai ro da zo'u broda gi ganai su'o da zo'u brode gi su'o da zo'u ge broda gi brode
5	4	cur 59	1 ⊢ ganai ge ro da zo'u broda gi su'o da zo'u brode gi su'o da zo'u ge broda gi brode

Colors of variables: sumti selbri bridi

Syntax hints: ganai bgan 9 ge bge 47 ro brd 222 su'o bsd 416

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 ax-gen1 224 ax-spec1 228 ax-qi1 234 ax-ro1-nf 249 ax-eb 420 ax-eq 422

This theorem depends on definitions: df-go 83

This theorem is referenced by: equs4 455