Theorem elini 4179

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 3947	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
4	1, 2, 3	mpbir2an 711	1 ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶)

Syntax hints:   ∈ wcel 2107   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-in 3938

This theorem is referenced by:  isfin1-3  10408  setc2ohom  18111  isdrs2  18322  fpwipodrs  18554  0cmp  23348  comppfsc  23486  ptcmpfi  23767  alexsubALTlem2  24002  alexsubALTlem4  24004  ptcmp  24012  cnstrcvs  25110  cncvs  25114  recvs  25115  recvsOLD  25116  qcvs  25117  cnncvs  25129  ovolicc1  25487  ioorf  25544  zringpid  33515  corclrcl  43682  0pwfi  45021  sge0rnn0  46340  sge0reuz  46419  termc2  49129