Theorem psssstrd

Description: Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	psssstrd.1	$$⊢\phi \to A\subset B$$
	psssstrd.2	$$⊢\phi \to B\subseteq C$$
Assertion	psssstrd	$$⊢\phi \to A\subset C$$

Proof

Step	Hyp	Ref	Expression
1		psssstrd.1	$$⊢\phi \to A\subset B$$
2		psssstrd.2	$$⊢\phi \to B\subseteq C$$
3		psssstr	$$⊢\left(A\subset B\wedge B\subseteq C\right)\to A\subset C$$
4	1 2 3	syl2anc	$$⊢\phi \to A\subset C$$