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