Theorem ssini

Description: An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003)

	Ref	Expression
Hypotheses	ssini.1	$$⊢A\subseteq B$$
	ssini.2	$$⊢A\subseteq C$$
Assertion	ssini	$$⊢A\subseteq B\cap C$$

Proof

Step	Hyp	Ref	Expression
1		ssini.1	$$⊢A\subseteq B$$
2		ssini.2	$$⊢A\subseteq C$$
3	1 2	pm3.2i	$$⊢\left(A\subseteq B\wedge A\subseteq C\right)$$
4		ssin	$$⊢\left(A\subseteq B\wedge A\subseteq C\right)\leftrightarrow A\subseteq B\cap C$$
5	3 4	mpbi	$$⊢A\subseteq B\cap C$$