bi2 - brismu bridi

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

Theorem bi2 58

Description: Property of biconditionals. (Contributed by la korvo, 31-Jul-2023.)

**Assertion**
Ref	Expression
bi2	⊢ ganai go broda gi brode gi ganai brode gi broda

**Proof of Theorem bi2**
Step	Hyp	Ref	Expression
1		df-go 52	. . 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
2	1	ge-lei 37	. 2 ⊢ ganai go broda gi brode gi ge ganai broda gi brode gi ganai brode gi broda
3	2	ge-red 40	1 ⊢ ganai go broda gi brode gi ganai brode gi broda

Colors of variables: sumti selbri bridi

Syntax hints: ganai bgan 9 ge bge 33 go bgo 51

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 14 ax-ge-le 34 ax-ge-re 35

This theorem depends on definitions: df-go 52

This theorem is referenced by: go-com-lem 64