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	1	a1i	$$⊢\phi \to B\subseteq A$$
4	3 2	sseqtrrd	$$⊢\phi \to B\subseteq C$$