Theorem elini 4123

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

Hypotheses

Ref	Expression
elini.1	⊢ 𝐴 ∈ 𝐵
elini.2	⊢ 𝐴 ∈ 𝐶

Assertion

Ref	Expression
elini	⊢ 𝐴 ∈ (𝐵 ∩ 𝐶)

Proof of Theorem elini

Step	Hyp	Ref	Expression
1		elini.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		elini.2	. 2 ⊢ 𝐴 ∈ 𝐶
3		elin 3899	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
4	1, 2, 3	mpbir2an 707	1 ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶)

Syntax hints:   ∈ wcel 2108   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  isfin1-3  10073  setc2ohom  17726  isdrs2  17939  fpwipodrs  18173  0cmp  22453  comppfsc  22591  ptcmpfi  22872  alexsubALTlem2  23107  alexsubALTlem4  23109  ptcmp  23117  cnstrcvs  24210  cncvs  24214  recvs  24215  qcvs  24216  cnncvs  24228  ovolicc1  24585  ioorf  24642  corclrcl  41204  0pwfi  42496  sge0rnn0  43796  sge0reuz  43875