Theorem ttcss2

Description: The subclass relationship is inherited by transitive closures. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcss2	Could not format assertion : No typesetting found for |- ( A C_ B -> TC+ A C_ TC+ B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ttcid	Could not format B C_ TC+ B : No typesetting found for |- B C_ TC+ B with typecode |-
2		sstr	Could not format ( ( A C_ B /\ B C_ TC+ B ) -> A C_ TC+ B ) : No typesetting found for |- ( ( A C_ B /\ B C_ TC+ B ) -> A C_ TC+ B ) with typecode |-
3	1 2	mpan2	Could not format ( A C_ B -> A C_ TC+ B ) : No typesetting found for |- ( A C_ B -> A C_ TC+ B ) with typecode |-
4		ttcss	Could not format ( A C_ TC+ B -> TC+ A C_ TC+ B ) : No typesetting found for |- ( A C_ TC+ B -> TC+ A C_ TC+ B ) with typecode |-
5	3 4	syl	Could not format ( A C_ B -> TC+ A C_ TC+ B ) : No typesetting found for |- ( A C_ B -> TC+ A C_ TC+ B ) with typecode |-