Theorem elini 4135

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

Syntax hints:   ∈ wcel 2119   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-in 3897

This theorem is referenced by:  isfin1-3  10306  setc2ohom  18060  isdrs2  18270  fpwipodrs  18504  0cmp  23384  comppfsc  23522  ptcmpfi  23803  alexsubALTlem2  24038  alexsubALTlem4  24040  ptcmp  24048  cnstrcvs  25133  cncvs  25137  recvs  25138  qcvs  25139  cnncvs  25151  ovolicc1  25508  ioorf  25565  zringpid  33642  corclrcl  44158  0pwfi  45514  sge0rnn0  46818  sge0reuz  46897  nthrucw  47338  termc2  50015