Metamath Proof Explorer

Theorem elttctr

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

Ref Expression
Assertion elttctr 
|- ( ( A e. TC+ B /\ B e. TC+ C ) -> A e. TC+ C )

Proof

Step Hyp Ref Expression
1 ttcel 
 |-  ( B e. TC+ C -> TC+ B C_ TC+ C )
2 1 sseld 
 |-  ( B e. TC+ C -> ( A e. TC+ B -> A e. TC+ C ) )
3 2 impcom 
 |-  ( ( A e. TC+ B /\ B e. TC+ C ) -> A e. TC+ C )