Theorem psstrd

Description: Proper subclass inclusion is transitive. Deduction form of psstr . (Contributed by David Moews, 1-May-2017)

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

Proof

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