Theorem eqsstrri

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999)

	Ref	Expression
Hypotheses	eqsstr3.1	$$⊢B=A$$
	eqsstr3.2	$$⊢B\subseteq C$$
Assertion	eqsstrri	$$⊢A\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		eqsstr3.1	$$⊢B=A$$
2		eqsstr3.2	$$⊢B\subseteq C$$
3	1	eqcomi	$$⊢A=B$$
4	3 2	eqsstri	$$⊢A\subseteq C$$