Theorem elini 4131

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

Syntax hints:   ∈ wcel 2121   ∩ cin 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-in 3892

This theorem is referenced by:  isfin1-3  10303  setc2ohom  18057  isdrs2  18267  fpwipodrs  18501  0cmp  23381  comppfsc  23519  ptcmpfi  23800  alexsubALTlem2  24035  alexsubALTlem4  24037  ptcmp  24045  cnstrcvs  25130  cncvs  25134  recvs  25135  qcvs  25136  cnncvs  25148  ovolicc1  25505  ioorf  25562  zringpid  33647  corclrcl  44166  0pwfi  45522  sge0rnn0  46825  sge0reuz  46904  nthrucw  47345  termc2  50022