Theorem simprll 778

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprll	⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Proof of Theorem simprll

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 728	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  fcof1  7221  mpo0  7431  fpr3g  8215  fprresex  8240  eroveu  8736  boxriin  8864  fofinf1o  9216  finsschain  9243  suppeqfsuppbi  9263  fsuppunbi  9273  marypha1lem  9317  wemapsolem  9436  wemapso  9437  wemapso2lem  9438  cantnf  9583  iunfictbso  10005  enfin2i  10212  ttukeylem7  10406  fpwwe2lem2  10523  fpwwe2lem8  10529  fpwwe2lem11  10532  fpwwelem  10536  distrlem4pr  10917  mulcmpblnr  10962  prsrlem1  10963  dedekind  11276  divdivdiv  11822  divmuleq  11826  divadddiv  11836  divsubdiv  11837  lediv12a  12015  xmullem  13163  xlemul1a  13187  seqcaopr  13946  leexp2r  14081  hashf1lem1  14362  hashf1lem2  14363  ccatsymb  14490  wrd2ind  14630  cshweqrep  14728  rtrclreclem4  14968  lo1le  15559  summolem2  15623  summo  15624  prodmolem2  15842  prodmo  15843  bezoutlem3  16452  bezoutlem4  16453  qredeu  16569  pcadd  16801  prmreclem2  16829  vdwlem9  16901  vdwlem10  16902  ramub1lem2  16939  ramub1  16940  prmgaplem7  16969  cofucl  17795  initoeu2  17923  setcmon  17994  poslubmo  18315  posglbmo  18316  rabsubmgmd  18612  issubmd  18714  grprcan  18886  isnsg3  19072  ghmpreima  19150  gaorber  19220  psgneu  19418  odcau  19516  lsmsubm  19565  lsmmod  19587  ablfaclem3  20001  rngpropd  20092  ringpropd  20206  lmodvsmmulgdi  20830  lmodprop2d  20857  lss1d  20896  lindff1  21757  islindf4  21775  assamulgscmlem2  21837  mplcoe1  21972  mplcoe5  21975  evlslem1  22017  mdetunilem7  22533  mdetunilem8  22534  mdetunilem9  22535  mdetuni0  22536  mdetmul  22538  cayhamlem3  22802  ppttop  22922  epttop  22924  cnhaus  23269  isreg2  23292  cncmp  23307  1stcfb  23360  2ndcomap  23373  1stccnp  23377  cldllycmp  23410  1stckgenlem  23468  txcls  23519  ptcnp  23537  txdis1cn  23550  txlly  23551  txnlly  23552  pthaus  23553  txhaus  23562  txkgen  23567  xkohaus  23568  xkococnlem  23574  xkococn  23575  opnfbas  23757  hausflimi  23895  hausflim  23896  hauspwpwf1  23902  alexsubALT  23966  tgpconncomp  24028  qustgplem  24036  metequiv2  24425  met2ndci  24437  nrmmetd  24489  nlmvscnlem1  24601  reconn  24744  xrge0tsms  24750  mulc1cncf  24825  ipcnlem1  25172  minveclem3  25356  pmltpc  25378  ovolicc2lem5  25449  ovolicc2  25450  uniioombllem6  25516  dyadmbllem  25527  vitalilem3  25538  mbfmullem  25653  itg2split  25677  itg2mono  25681  bddiblnc  25770  dvlip2  25927  lhop1  25946  dvcnvrelem1  25949  dvfsumrlim  25965  ftc1lem6  25975  itgsubst  25983  dgrco  26208  plyexmo  26248  ulmdvlem3  26338  abelthlem2  26369  abelthlem8  26376  mpodvdsmulf1o  27131  dvdsmulf1o  27133  chpchtsum  27157  dchrptlem2  27203  2sqlem5  27360  2sqlem9  27365  2sqb  27370  chpo1ubb  27419  vmadivsumb  27421  selbergb  27487  selberg2b  27490  selberg3lem2  27496  pntrsumbnd  27504  pntrlog2bnd  27522  pntibndlem3  27530  pnt3  27550  noresle  27636  nosupprefixmo  27639  noinfprefixmo  27640  nosupbday  27644  noinfbday  27659  noinfbnd1lem5  27666  addsprop  27919  mulsproplem9  28063  mulsasslem3  28104  expadds  28358  readdscl  28401  tgjustf  28451  hlcgreu  28596  mirreu3  28632  cgraswap  28798  cgracom  28800  cgratr  28801  flatcgra  28802  acopyeu  28812  axsegcon  28905  ax5seglem9  28915  axeuclid  28941  axcontlem10  28951  axcontlem12  28953  wwlksnredwwlkn0  29874  n4cyclfrgr  30271  frgrnbnb  30273  numclwwlk1lem2fo  30338  ablo4  30530  smcnlem  30677  pjhthmo  31282  pjpjpre  31399  lnconi  32013  resf1o  32713  mgcoval  32967  xrge0tsmsd  33042  erlval  33225  derangenlem  35215  pconnconn  35275  connpconn  35279  cvmfolem  35323  cvmliftmolem2  35326  cvmliftmo  35328  cvmliftlem7  35335  cvmlift2lem10  35356  cvmlift3lem8  35370  linecgr  36125  btwnconn1lem8  36138  btwnconn1lem14  36144  btwnconn3  36147  brsegle  36152  segletr  36158  segleantisym  36159  outsideofeq  36174  linethru  36197  finminlem  36362  nn0prpwlem  36366  neibastop2lem  36404  weiunpo  36509  mblfinlem3  37709  ftc1cnnc  37742  isbnd3  37834  cvlcvr1  39448  athgt  39565  4atlem12  39721  paddasslem12  39940  paddasslem13  39941  cdleme0cp  40323  cdleme42keg  40595  cdleme42mgN  40597  trlord  40678  cdlemg6c  40729  cdlemkid4  41043  dihopelvalcpre  41357  dihmeetlem1N  41399  dihglblem5apreN  41400  dihmeetlem4preN  41415  dihmeetlem6  41418  dihmeetlem10N  41425  dihmeetlem11N  41426  dihmeetlem13N  41428  dihjatcclem4  41530  fsuppssind  42696  prjspner1  42729  mzpcl1  42832  mzpcompact2lem  42854  diophin  42875  pell14qrmulcl  42966  pwssplit4  43192  hbtlem2  43227  iunrelexpuztr  43822  stoweidlem57  46165  stoweidlem61  46169  fourierdlem92  46306  euoreqb  47219  prproropf1olem3  47615  prproropf1olem4  47616  fpprwpprb  47850  cycldlenngric  48038  grimgrtri  48059  2zlidl  48350  lmodvsmdi  48489  2arwcat  49711