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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906

This theorem is used by:  isfin1-3  10388  setc2ohom  18184  isdrs2  18394  fpwipodrs  18628  0cmp  23619  comppfsc  23758  ptcmpfi  24039  alexsubALTlem2  24274  alexsubALTlem4  24276  ptcmp  24284  cnstrcvs  25369  cncvs  25373  recvs  25374  qcvs  25375  cnncvs  25387  ovolicc1  25744  ioorf  25801  zringpid  33962  corclrcl  44547  0pwfi  45893  sge0rnn0  47196  sge0reuz  47275  numtowerdt  47734  termc2  50444