psssstr

Description: Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996)

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

Step	Hyp	Ref	Expression
1		sspss	$⊢ B \subseteq C \leftrightarrow (B \subset C \lor B = C)$
2		psstr	$⊢ (A \subset B \land B \subset C) \to A \subset C$
3	2	ex	$⊢ A \subset B \to (B \subset C \to A \subset C)$
4		psseq2	$⊢ B = C \to (A \subset B \leftrightarrow A \subset C)$
5	4	biimpcd	$⊢ A \subset B \to (B = C \to A \subset C)$
6	3 5	jaod	$⊢ A \subset B \to ((B \subset C \lor B = C) \to A \subset C)$
7	6	imp	$⊢ (A \subset B \land (B \subset C \lor B = C)) \to A \subset C$
8	1 7	sylan2b	$⊢ (A \subset B \land B \subseteq C) \to A \subset C$

Metamath Proof Explorer