This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
Assertion elin2d ( 𝜑 → 𝑋 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 elin1d.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
2 elinel2 ⊢ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑋 ∈ 𝐵 )
3 1 2 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )