Theorem sstr

Description: Transitivity of subclass relationship. Theorem 6 of Suppes p. 23. (Contributed by NM, 5-Sep-2003)

	Ref	Expression
Assertion	sstr	$$⊢\left(A\subseteq B\wedge B\subseteq C\right)\to A\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		sstr2	$$⊢A\subseteq B\to \left(B\subseteq C\to A\subseteq C\right)$$
2	1	imp	$$⊢\left(A\subseteq B\wedge B\subseteq C\right)\to A\subseteq C$$