syl5bi - brismu bridi

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

Theorem syl5bi 86

Description: Replace a nested antecedent using a biconditional. (Contributed by la korvo, 22-Jun-2024.)

**Hypotheses**
Ref	Expression
syl5bi.0	⊢ go broda gi brode
syl5bi.1	⊢ ganai brodi gi ganai brode gi brodo

**Assertion**
Ref	Expression
syl5bi	⊢ ganai brodi gi ganai broda gi brodo

**Proof of Theorem syl5bi**
Step	Hyp	Ref	Expression
1		syl5bi.0	. . 3 ⊢ go broda gi brode
2	1	go-ganai 63	. 2 ⊢ ganai broda gi brode
3		syl5bi.1	. 2 ⊢ ganai brodi gi ganai brode gi brodo
4	2, 3	syl5 30	1 ⊢ ganai brodi gi ganai broda gi brodo

Colors of variables: sumti selbri bridi

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15 ax-ge-le 43

This theorem depends on definitions: df-go 61

This theorem is referenced by: subeq-lem2 393