Theorem elini 4174

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

Syntax hints:   ∈ wcel 2108   ∩ cin 3925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933

This theorem is referenced by:  isfin1-3  10400  setc2ohom  18108  isdrs2  18318  fpwipodrs  18550  0cmp  23332  comppfsc  23470  ptcmpfi  23751  alexsubALTlem2  23986  alexsubALTlem4  23988  ptcmp  23996  cnstrcvs  25092  cncvs  25096  recvs  25097  recvsOLD  25098  qcvs  25099  cnncvs  25111  ovolicc1  25469  ioorf  25526  zringpid  33567  corclrcl  43731  0pwfi  45083  sge0rnn0  46397  sge0reuz  46476  termc2  49403