Theorem elinel2 4029

Description: Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
elinel2	⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Proof of Theorem elinel2

Step	Hyp	Ref	Expression
1		elin 4025	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simprbi 492	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2164   ∩ cin 3797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805

This theorem is referenced by:  elin2d  4032  eldmeldmressn  5681  onfr  6006  wfrlem4  7688  ncvsge0  23329  cphsscph  23426  itg2cnlem2  23935  uhgrspansubgrlem  26594  disjin2  29943  partfun  30019  xrge0tsmsd  30326  frrlem4  32317  heicant  33983  mndoisexid  34205  eqvreldisj  34899  fiinfi  38714  restuni3  40111  nel2nelin  40143  disjinfi  40183  inmap  40202  iocopn  40536  icoopn  40541  icomnfinre  40568  uzinico  40576  islpcn  40660  lptre2pt  40661  limcresiooub  40663  limcresioolb  40664  limclner  40672  limsupmnflem  40741  limsupresxr  40787  liminfresxr  40788  liminfvalxr  40804  icccncfext  40889  stoweidlem39  41044  stoweidlem50  41055  stoweidlem57  41062  fourierdlem32  41144  fourierdlem33  41145  fourierdlem48  41159  fourierdlem49  41160  fourierdlem71  41182  fourierdlem80  41191  qndenserrnbllem  41299  sge0rnre  41366  sge0z  41377  sge0tsms  41382  sge0cl  41383  sge0f1o  41384  sge0fsum  41389  sge0sup  41393  sge0rnbnd  41395  sge0ltfirp  41402  sge0resplit  41408  sge0le  41409  sge0split  41411  sge0iunmptlemre  41417  sge0ltfirpmpt2  41428  sge0isum  41429  sge0xaddlem1  41435  sge0xaddlem2  41436  sge0pnffsumgt  41444  sge0gtfsumgt  41445  sge0uzfsumgt  41446  sge0seq  41448  sge0reuz  41449  meadjiunlem  41467  caragendifcl  41516  omeiunltfirp  41521  carageniuncllem2  41524  caratheodorylem2  41529  hspmbllem2  41629  pimiooltgt  41709  pimdecfgtioc  41713  pimincfltioc  41714  pimdecfgtioo  41715  pimincfltioo  41716  sssmf  41735  smfaddlem1  41759  smfaddlem2  41760  smfadd  41761  mbfpsssmf  41779  smfmullem4  41789  smfmul  41790  smfdiv  41792  smfsuplem1  41805  smfliminflem  41824  fmtno4prm  42331  rnghmsubcsetclem2  42837  rhmsubcsetclem2  42883  rhmsubcrngclem2  42889