Metamath Proof Explorer

Theorem ssttctr

Description: Transitivity of A C_ TC+ B relationship. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion ssttctr 
|- ( ( A C_ TC+ B /\ B C_ TC+ C ) -> A C_ TC+ C )

Proof

Step Hyp Ref Expression
1 ttcss 
 |-  ( B C_ TC+ C -> TC+ B C_ TC+ C )
2 sstr 
 |-  ( ( A C_ TC+ B /\ TC+ B C_ TC+ C ) -> A C_ TC+ C )
3 1 2 sylan2 
 |-  ( ( A C_ TC+ B /\ B C_ TC+ C ) -> A C_ TC+ C )