foml19.41 - brismu bridi

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

Theorem foml19.41 434

Description: Obsolete version of theorem 19.41 of [Margaris] p. 90. (Contributed by la korvo, 9-Jul-2025.)

**Hypothesis**
Ref	Expression
foml19.41.0	⊢ ganai brode gi ro da zo'u brode

**Assertion**
Ref	Expression
foml19.41	⊢ go su'o da zo'u ge broda gi brode gi ge su'o da zo'u broda gi brode

**Proof of Theorem foml19.41**
Step	Hyp	Ref	Expression
1		ge-dist-ex 433	. . 3 ⊢ ganai su'o da zo'u ge broda gi brode gi ge su'o da zo'u broda gi su'o da zo'u brode
2		foml19.41.0	. . . . 5 ⊢ ganai brode gi ro da zo'u brode
3		id 19	. . . . 5 ⊢ ganai brode gi brode
4	2, 3	exlimih 426	. . . 4 ⊢ ganai su'o da zo'u brode gi brode
5	4	ge-pairr 81	. . 3 ⊢ ganai ge su'o da zo'u broda gi su'o da zo'u brode gi ge su'o da zo'u broda gi brode
6	1, 5	syl 21	. 2 ⊢ ganai su'o da zo'u ge broda gi brode gi ge su'o da zo'u broda gi brode
7		ge-in-swap12 58	. . . 4 ⊢ ganai brode gi ganai broda gi ge broda gi brode
8	2, 7	eximdh 430	. . 3 ⊢ ganai brode gi ganai su'o da zo'u broda gi su'o da zo'u ge broda gi brode
9	8	cur-swap12 60	. 2 ⊢ ganai ge su'o da zo'u broda gi brode gi su'o da zo'u ge broda gi brode
10	6, 9	iso 87	1 ⊢ go su'o da zo'u ge broda gi brode gi ge su'o da zo'u broda gi brode

Colors of variables: sumti selbri bridi

Syntax hints: ge bge 47 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: subh 461