Metamath Proof Explorer


Theorem elind

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

Ref Expression
Hypotheses elind.1 φ X A
elind.2 φ X B
Assertion elind φ X A B

Proof

Step Hyp Ref Expression
1 elind.1 φ X A
2 elind.2 φ X B
3 elin X A B X A X B
4 1 2 3 sylanbrc φ X A B