go-syl - brismu bridi

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

Theorem go-syl 100

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

Colors of variables: sumti selbri bridi

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

This theorem is referenced by: e-com 150 a-com 187 o-com 201 du-trans 257 dunli-sym 370 mintu-sym 377