Theorem ssinss2d

Description: Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	ssinss2d.1	$$⊢\phi \to B\subseteq C$$
Assertion	ssinss2d	$$⊢\phi \to A\cap B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		ssinss2d.1	$$⊢\phi \to B\subseteq C$$
2		incom	$$⊢A\cap B=B\cap A$$
3	1	ssinss1d	$$⊢\phi \to B\cap A\subseteq C$$
4	2 3	eqsstrid	$$⊢\phi \to A\cap B\subseteq C$$