go-syl - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > go-syl

Theorem go-syl 68

Description: {go} admits composition. (Contributed by la korvo, 16-Aug-2023.)

**Hypotheses**
Ref	Expression
go-syl.0	⊢ go broda gi brode
go-syl.1	⊢ go brode gi brodi

**Assertion**
Ref	Expression
go-syl	⊢ go broda gi brodi

**Proof of Theorem go-syl**
Step	Hyp	Ref	Expression
1		go-syl.0	. 2 ⊢ go broda gi brode
2		go-syl.1	. 2 ⊢ go brode gi brodi
3	1, 2	ax-go-trans 67	1 ⊢ go broda gi brodi

Colors of variables: sumti selbri bridi

This theorem was proved from axioms: ax-go-trans 67

This theorem is referenced by: a-com 142 o-com 156 du-trans 203 dunli-sym 296 mintu-sym 303