Theorem sseqtrdi

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004)

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

Proof

Step	Hyp	Ref	Expression
1		sseqtrdi.1	$$⊢\phi \to A\subseteq B$$
2		sseqtrdi.2	$$⊢B=C$$
3	2	sseq2i	$$⊢A\subseteq B\leftrightarrow A\subseteq C$$
4	1 3	sylib	$$⊢\phi \to A\subseteq C$$