Theorem elini

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

	Ref	Expression
Hypotheses	elini.1	|- A e. B
	elini.2	|- A e. C
Assertion	elini	|- A e. ( B i^i C )

Proof

Step	Hyp	Ref	Expression
1		elini.1	|- A e. B
2		elini.2	|- A e. C
3		elin	|- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )
4	1 2 3	mpbir2an	|- A e. ( B i^i C )