Theorem elttctr

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

	Ref	Expression
Assertion	elttctr	⊢ ( ( 𝐴 ∈ TC+ 𝐵 ∧ 𝐵 ∈ TC+ 𝐶 ) → 𝐴 ∈ TC+ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		ttcel	⊢ ( 𝐵 ∈ TC+ 𝐶 → TC+ 𝐵 ⊆ TC+ 𝐶 )
2	1	sseld	⊢ ( 𝐵 ∈ TC+ 𝐶 → ( 𝐴 ∈ TC+ 𝐵 → 𝐴 ∈ TC+ 𝐶 ) )
3	2	impcom	⊢ ( ( 𝐴 ∈ TC+ 𝐵 ∧ 𝐵 ∈ TC+ 𝐶 ) → 𝐴 ∈ TC+ 𝐶 )