Theorem elini 4193

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

Syntax hints:   ∈ wcel 2099   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954

This theorem is referenced by:  isfin1-3  10410  setc2ohom  18084  isdrs2  18298  fpwipodrs  18532  0cmp  23311  comppfsc  23449  ptcmpfi  23730  alexsubALTlem2  23965  alexsubALTlem4  23967  ptcmp  23975  cnstrcvs  25081  cncvs  25085  recvs  25086  recvsOLD  25087  qcvs  25088  cnncvs  25100  ovolicc1  25458  ioorf  25515  corclrcl  43137  0pwfi  44423  sge0rnn0  45756  sge0reuz  45835