Theorem elini 4145

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

This proof depends on syntax axioms:   ∈ wcel 2145   ∩ cin 3898

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906

This theorem is used by:  isfin1-3  10457  setc2ohom  18263  isdrs2  18473  fpwipodrs  18707  0cmp  23705  comppfsc  23844  ptcmpfi  24125  alexsubALTlem2  24360  alexsubALTlem4  24362  ptcmp  24370  cnstrcvs  25455  cncvs  25459  recvs  25460  qcvs  25461  cnncvs  25473  ovolicc1  25830  ioorf  25887  zringpid  34077  corclrcl  44692  0pwfi  46045  sge0rnn0  47347  sge0reuz  47426  numtowerdt  47885  termc2  50595