Theorem ssind

Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		ssind.1	$$⊢\phi \to A\subseteq B$$
2		ssind.2	$$⊢\phi \to A\subseteq C$$
3	1 2	jca	$$⊢\phi \to \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	sylib	$$⊢\phi \to A\subseteq B\cap C$$