Theorem elinel2 4101

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 4091

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 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-in 4093

This theorem is used by:  elin2d  4104  nel2nelin  4107  eldmeldmressn  6019  onfr  6408  partfun  6694  fvcofneq  7101  offres  8002  fsplitfpar  8139  ressuppss  8211  frrlem4  8318  frrlem11  8325  frrlem12  8326  smores3  8372  erdisj  8786  dffi2  9425  r0weon  10101  fodomfi2  10149  ackbij1lem6  10312  ackbij1lem9  10315  ackbij1lem10  10316  ackbij1lem11  10317  ackbij1lem18  10324  isfin1-3  10474  dedekindle  11484  uzdisj  13741  nn0disj  13788  rlimres  15737  lo1res  15738  ackbijnn  16009  bitsinv2  16625  bitsf1ocnv  16626  smueqlem  16672  prmrec  17112  isstruct2  17339  isacs2  17839  isdrs2  18492  isacs3lem  18728  subrngpropd  20832  subrgpropd  20872  rnghmsubcsetclem2  20896  rhmsubcsetclem2  20925  rhmsubcrngclem2  20931  sralmod  21474  basdif0  23283  clsval2  23380  mreclatdemoBAD  23426  restfpw  23509  fincmp  23723  discmp  23728  uncmp  23733  cmpfi  23738  bwth  23740  iunconn  23758  1stcrest  23783  infil  24194  alexsublem  24375  alexsubALTlem3  24380  tsmsfbas  24459  tsmsgsum  24470  tsmssubm  24474  tsmsres  24475  tsmsf1o  24476  tsmsmhm  24477  tsmsadd  24478  tsmsxplem1  24484  tsmsxp  24486  blres  24762  reconnlem2  25159  xrge0tsms  25166  ncvsge0  25486  cphsscph  25584  cfilres  25629  ioombl1lem4  25894  mbfadd  25994  mbfsub  25995  mbfmul  26059  itg2cnlem2  26095  bddmulibl  26171  ellimc2  26209  fsumvma2  27553  vmasum  27555  chpchtsum  27558  chebbnd1lem1  27808  dirith2  27867  uhgrspansubgrlem  29883  disjin2  33235  xrge0tsmsd  33687  cmpcref  34535  prsdm  34599  prsrn  34600  pibt2  38480  heicant  38713  mndoisexid  38943  eqvreldisj  39770  eldisjsim2  40007  fiinfi  44714  ismnushort  45425  hfstructfun  46165  rnhfstructsshf  46166  restuni3  46272  disjinfi  46346  inmap  46361  iocopn  46671  icoopn  46676  icomnfinre  46703  uzinico  46710  islpcn  46788  lptre2pt  46789  limcresiooub  46791  limcresioolb  46792  limclner  46800  limsupmnflem  46869  limsupresxr  46915  liminfresxr  46916  liminfvalxr  46932  icccncfext  47036  stoweidlem39  47188  stoweidlem50  47199  stoweidlem57  47206  fourierdlem32  47288  fourierdlem33  47289  fourierdlem48  47303  fourierdlem49  47304  fourierdlem71  47326  fourierdlem80  47335  qndenserrnbllem  47443  sge0rnre  47513  sge0z  47524  sge0tsms  47529  sge0cl  47530  sge0f1o  47531  sge0fsum  47536  sge0sup  47540  sge0rnbnd  47542  sge0ltfirp  47549  sge0resplit  47555  sge0le  47556  sge0split  47558  sge0iunmptlemre  47564  sge0ltfirpmpt2  47575  sge0isum  47576  sge0xaddlem1  47582  sge0xaddlem2  47583  sge0pnffsumgt  47591  sge0gtfsumgt  47592  sge0uzfsumgt  47593  sge0seq  47595  sge0reuz  47596  meadjiunlem  47614  caragendifcl  47663  omeiunltfirp  47668  carageniuncllem2  47671  caratheodorylem2  47676  hspmbllem2  47776  pimiooltgt  47859  pimdecfgtioc  47864  pimincfltioc  47865  pimdecfgtioo  47866  pimincfltioo  47867  sssmf  47887  smfaddlem1  47912  smfaddlem2  47913  smfadd  47914  mbfpsssmf  47932  smfmullem4  47943  smfmul  47944  smfdiv  47946  smfsuplem1  47960  smfliminflem  47979  fmtno4prm  48799