Theorem elini 4153

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

Syntax hints:   ∈ wcel 2143   ∩ cin 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3913

This theorem is referenced by:  isfin1-3  10371  setc2ohom  18153  isdrs2  18363  fpwipodrs  18597  0cmp  23532  comppfsc  23670  ptcmpfi  23951  alexsubALTlem2  24186  alexsubALTlem4  24188  ptcmp  24196  cnstrcvs  25281  cncvs  25285  recvs  25286  qcvs  25287  cnncvs  25299  ovolicc1  25656  ioorf  25713  zringpid  33823  corclrcl  44416  0pwfi  45762  sge0rnn0  47065  sge0reuz  47144  nthrucw  47590  termc2  50279