Theorem ssinss1d

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

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

Proof

Step	Hyp	Ref	Expression
1		ssinss1d.1	$$⊢\phi \to A\subseteq C$$
2		ssinss1	$$⊢A\subseteq C\to A\cap B\subseteq C$$
3	1 2	syl	$$⊢\phi \to A\cap B\subseteq C$$