Theorem elinel2 4102

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by:  elin2d  4105  nel2nelin  4108  eldmeldmressn  6032  onfr  6428  partfun  6716  fvcofneq  7125  offres  8029  fsplitfpar  8166  ressuppss  8238  frrlem4  8345  frrlem11  8352  frrlem12  8353  smores3  8399  erdisj  8813  dffi2  9452  r0weon  10130  fodomfi2  10178  ackbij1lem6  10341  ackbij1lem9  10344  ackbij1lem10  10345  ackbij1lem11  10346  ackbij1lem18  10353  isfin1-3  10503  dedekindle  11513  uzdisj  13771  nn0disj  13818  rlimres  15769  lo1res  15770  ackbijnn  16041  bitsinv2  16657  bitsf1ocnv  16658  smueqlem  16704  prmrec  17144  isstruct2  17371  isacs2  17877  isdrs2  18530  isacs3lem  18766  subrngpropd  20871  subrgpropd  20911  rnghmsubcsetclem2  20935  rhmsubcsetclem2  20964  rhmsubcrngclem2  20970  sralmod  21513  basdif0  23326  clsval2  23423  mreclatdemoBAD  23469  restfpw  23552  fincmp  23766  discmp  23771  uncmp  23776  cmpfi  23781  bwth  23783  iunconn  23801  1stcrest  23826  infil  24237  alexsublem  24418  alexsubALTlem3  24423  tsmsfbas  24502  tsmsgsum  24513  tsmssubm  24517  tsmsres  24518  tsmsf1o  24519  tsmsmhm  24520  tsmsadd  24521  tsmsxplem1  24527  tsmsxp  24529  blres  24805  reconnlem2  25202  xrge0tsms  25209  ncvsge0  25529  cphsscph  25627  cfilres  25672  ioombl1lem4  25937  mbfadd  26037  mbfsub  26038  mbfmul  26102  itg2cnlem2  26138  bddmulibl  26214  ellimc2  26252  fsumvma2  27598  vmasum  27600  chpchtsum  27603  chebbnd1lem1  27853  dirith2  27912  uhgrspansubgrlem  29928  disjin2  33279  xrge0tsmsd  33733  cmpcref  34593  prsdm  34657  prsrn  34658  pibt2  38608  heicant  38841  mndoisexid  39069  eqvreldisj  39896  eldisjsim2  40133  fiinfi  44835  ismnushort  45546  hfstructfun  46293  rnhfstructsshf  46294  restuni3  46406  disjinfi  46480  inmap  46495  iocopn  46805  icoopn  46810  icomnfinre  46837  uzinico  46844  islpcn  46922  lptre2pt  46923  limcresiooub  46925  limcresioolb  46926  limclner  46934  limsupmnflem  47003  limsupresxr  47049  liminfresxr  47050  liminfvalxr  47066  icccncfext  47170  stoweidlem39  47322  stoweidlem50  47333  stoweidlem57  47340  fourierdlem32  47422  fourierdlem33  47423  fourierdlem48  47437  fourierdlem49  47438  fourierdlem71  47460  fourierdlem80  47469  qndenserrnbllem  47577  sge0rnre  47647  sge0z  47658  sge0tsms  47663  sge0cl  47664  sge0f1o  47665  sge0fsum  47670  sge0sup  47674  sge0rnbnd  47676  sge0ltfirp  47683  sge0resplit  47689  sge0le  47690  sge0split  47692  sge0iunmptlemre  47698  sge0ltfirpmpt2  47709  sge0isum  47710  sge0xaddlem1  47716  sge0xaddlem2  47717  sge0pnffsumgt  47725  sge0gtfsumgt  47726  sge0uzfsumgt  47727  sge0seq  47729  sge0reuz  47730  meadjiunlem  47748  caragendifcl  47797  omeiunltfirp  47802  carageniuncllem2  47805  caratheodorylem2  47810  hspmbllem2  47910  pimiooltgt  47993  pimdecfgtioc  47998  pimincfltioc  47999  pimdecfgtioo  48000  pimincfltioo  48001  sssmf  48021  smfaddlem1  48046  smfaddlem2  48047  smfadd  48048  mbfpsssmf  48066  smfmullem4  48077  smfmul  48078  smfdiv  48080  smfsuplem1  48094  smfliminflem  48113  fmtno4prm  48933