Metamath Proof Explorer

Theorem elin2d

Description: Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020)

Ref Expression
Hypothesis elin1d.1 φ X A B
Assertion elin2d φ X B


Step Hyp Ref Expression
1 elin1d.1 φ X A B
2 elinel2 X A B X B
3 1 2 syl φ X B