This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sstr

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

		Ref	Expression
	Assertion	sstr	$⊢ (A \subseteq B \land B \subseteq C) \to A \subseteq C$

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