Theorem elini

Description: Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	elini.1	$$⊢A\in B$$
	elini.2	$$⊢A\in C$$
Assertion	elini	$$⊢A\in \left(B\cap C\right)$$

Proof

Step	Hyp	Ref	Expression
1		elini.1	$$⊢A\in B$$
2		elini.2	$$⊢A\in C$$
3		elin	$$⊢A\in \left(B\cap C\right)\leftrightarrow \left(A\in B\wedge A\in C\right)$$
4	1 2 3	mpbir2an	$$⊢A\in \left(B\cap C\right)$$