Theorem elinel2 4148

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 3915	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simprbi 503	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∈ 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:  elin2d  4151  nel2nelin  4154  eldmeldmressn  6014  onfr  6402  partfun  6686  fvcofneq  7093  offres  7995  fsplitfpar  8129  ressuppss  8200  frrlem4  8307  frrlem11  8314  frrlem12  8315  smores3  8361  erdisj  8775  dffi2  9415  r0weon  10091  fodomfi2  10139  ackbij1lem6  10302  ackbij1lem9  10305  ackbij1lem10  10306  ackbij1lem11  10307  ackbij1lem18  10314  isfin1-3  10464  dedekindle  11474  uzdisj  13731  nn0disj  13778  rlimres  15725  lo1res  15726  ackbijnn  15997  bitsinv2  16613  bitsf1ocnv  16614  smueqlem  16660  prmrec  17100  isstruct2  17327  isacs2  17827  isdrs2  18480  isacs3lem  18716  subrngpropd  20820  subrgpropd  20860  rnghmsubcsetclem2  20884  rhmsubcsetclem2  20913  rhmsubcrngclem2  20919  sralmod  21462  basdif0  23271  clsval2  23368  mreclatdemoBAD  23414  restfpw  23497  fincmp  23711  discmp  23716  uncmp  23721  cmpfi  23726  bwth  23728  iunconn  23746  1stcrest  23771  infil  24182  alexsublem  24363  alexsubALTlem3  24368  tsmsfbas  24447  tsmsgsum  24458  tsmssubm  24462  tsmsres  24463  tsmsf1o  24464  tsmsmhm  24465  tsmsadd  24466  tsmsxplem1  24472  tsmsxp  24474  blres  24750  reconnlem2  25147  xrge0tsms  25154  ncvsge0  25474  cphsscph  25572  cfilres  25617  ioombl1lem4  25882  mbfadd  25982  mbfsub  25983  mbfmul  26047  itg2cnlem2  26083  bddmulibl  26159  ellimc2  26197  fsumvma2  27541  vmasum  27543  chpchtsum  27546  chebbnd1lem1  27796  dirith2  27855  uhgrspansubgrlem  29871  disjin2  33181  xrge0tsmsd  33634  prsdm  34546  prsrn  34547  pibt2  38340  heicant  38573  mndoisexid  38803  eqvreldisj  39630  eldisjsim2  39867  fiinfi  44573  ismnushort  45284  hfstructfun  46025  rnhfstructsshf  46026  restuni3  46132  disjinfi  46206  inmap  46221  iocopn  46531  icoopn  46536  icomnfinre  46563  uzinico  46570  islpcn  46648  lptre2pt  46649  limcresiooub  46651  limcresioolb  46652  limclner  46660  limsupmnflem  46729  limsupresxr  46775  liminfresxr  46776  liminfvalxr  46792  icccncfext  46896  stoweidlem39  47048  stoweidlem50  47059  stoweidlem57  47066  fourierdlem32  47148  fourierdlem33  47149  fourierdlem48  47163  fourierdlem49  47164  fourierdlem71  47186  fourierdlem80  47195  qndenserrnbllem  47303  sge0rnre  47373  sge0z  47384  sge0tsms  47389  sge0cl  47390  sge0f1o  47391  sge0fsum  47396  sge0sup  47400  sge0rnbnd  47402  sge0ltfirp  47409  sge0resplit  47415  sge0le  47416  sge0split  47418  sge0iunmptlemre  47424  sge0ltfirpmpt2  47435  sge0isum  47436  sge0xaddlem1  47442  sge0xaddlem2  47443  sge0pnffsumgt  47451  sge0gtfsumgt  47452  sge0uzfsumgt  47453  sge0seq  47455  sge0reuz  47456  meadjiunlem  47474  caragendifcl  47523  omeiunltfirp  47528  carageniuncllem2  47531  caratheodorylem2  47536  hspmbllem2  47636  pimiooltgt  47719  pimdecfgtioc  47724  pimincfltioc  47725  pimdecfgtioo  47726  pimincfltioo  47727  sssmf  47747  smfaddlem1  47772  smfaddlem2  47773  smfadd  47774  mbfpsssmf  47792  smfmullem4  47803  smfmul  47804  smfdiv  47806  smfsuplem1  47820  smfliminflem  47839  fmtno4prm  48659