Theorem elini 4152

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 724	1 ⊢ 𝐴 ∈ (𝐵 ∩ 𝐶)

This proof depends on syntax axioms:   ∈ wcel 2146   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  isfin1-3  10381  setc2ohom  18169  isdrs2  18379  fpwipodrs  18613  0cmp  23580  comppfsc  23718  ptcmpfi  23999  alexsubALTlem2  24234  alexsubALTlem4  24236  ptcmp  24244  cnstrcvs  25329  cncvs  25333  recvs  25334  qcvs  25335  cnncvs  25347  ovolicc1  25704  ioorf  25761  zringpid  33865  corclrcl  44466  0pwfi  45812  sge0rnn0  47115  sge0reuz  47194  nthrucw  47640  termc2  50329