Theorem sseqtrrid

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

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

Proof

Step	Hyp	Ref	Expression
1		sseqtrrid.1	$$⊢B\subseteq A$$
2		sseqtrrid.2	$$⊢\phi \to C=A$$
3	2	eqcomd	$$⊢\phi \to A=C$$
4	1 3	sseqtrid	$$⊢\phi \to B\subseteq C$$