bi1 - brismu bridi

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

Theorem bi1 88

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

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

**Proof of Theorem bi1**
Step	Hyp	Ref	Expression
1		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
2	1	ge-lei 51	. 2 ⊢ ganai go broda gi brode gi ge ganai broda gi brode gi ganai brode gi broda
3	2	ge-led 52	1 ⊢ ganai go broda gi brode gi ganai 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-k 11 ax-s 15 ax-ge-le 48

This theorem depends on definitions: df-go 83

This theorem is referenced by: go-ganaid 91 go-com-lem 96