Theorem elini 4096

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

This proof depends on syntax axioms:   ∈ wcel 2144   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091

This theorem is used by:  isfin1-3  10468  setc2ohom  18276  isdrs2  18486  fpwipodrs  18720  0cmp  23718  comppfsc  23857  ptcmpfi  24138  alexsubALTlem2  24373  alexsubALTlem4  24375  ptcmp  24383  cnstrcvs  25468  cncvs  25472  recvs  25473  qcvs  25474  cnncvs  25486  ovolicc1  25843  ioorf  25900  zringpid  34131  corclrcl  44801  0pwfi  46170  sge0rnn0  47472  sge0reuz  47551  numtowerdt  48010  termc2  50747