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

Metamath Proof Explorer

Theorem elini

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

Ref Expression
Hypotheses elini.1 ⊢ A ∈ B
elini.2 ⊢ A ∈ C
Assertion elini ⊢ A ∈ B ∩ C

Proof

Step Hyp Ref Expression
1 elini.1 ⊢ A ∈ B
2 elini.2 ⊢ A ∈ C
3 elin ⊢ A ∈ B ∩ C ↔ A ∈ B ∧ A ∈ C
4 1 2 3 mpbir2an ⊢ A ∈ B ∩ C