Theorem sseqtrid

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		sseqtrid.1	$$⊢B\subseteq A$$
2		sseqtrid.2	$$⊢\phi \to A=C$$
3		sseq2	$$⊢A=C\to \left(B\subseteq A\leftrightarrow B\subseteq C\right)$$
4	3	biimpa	$$⊢\left(A=C\wedge B\subseteq A\right)\to B\subseteq C$$
5	2 1 4	sylancl	$$⊢\phi \to B\subseteq C$$