Theorem elind

Description: Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypotheses	elind.1	$$⊢\phi \to X\in A$$
	elind.2	$$⊢\phi \to X\in B$$
Assertion	elind	$$⊢\phi \to X\in \left(A\cap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elind.1	$$⊢\phi \to X\in A$$
2		elind.2	$$⊢\phi \to X\in B$$
3		elin	$$⊢X\in \left(A\cap B\right)\leftrightarrow \left(X\in A\wedge X\in B\right)$$
4	1 2 3	sylanbrc	$$⊢\phi \to X\in \left(A\cap B\right)$$