go-syl - brismu bridi

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

Theorem go-syl 78

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 77	1 ⊢ go broda gi brodi

Colors of variables: sumti selbri bridi

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

This theorem is referenced by: a-com 156 o-com 170 du-trans 221 dunli-sym 333 mintu-sym 340