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  7230  mpo0  7440  fpr3g  8224  fprresex  8249  eroveu  8745  boxriin  8873  fofinf1o  9226  finsschain  9253  suppeqfsuppbi  9273  fsuppunbi  9283  marypha1lem  9327  wemapsolem  9446  wemapso  9447  wemapso2lem  9448  cantnf  9593  iunfictbso  10015  enfin2i  10222  ttukeylem7  10416  fpwwe2lem2  10533  fpwwe2lem8  10539  fpwwe2lem11  10542  fpwwelem  10546  distrlem4pr  10927  mulcmpblnr  10972  prsrlem1  10973  dedekind  11286  divdivdiv  11832  divmuleq  11836  divadddiv  11846  divsubdiv  11847  lediv12a  12025  xmullem  13173  xlemul1a  13197  seqcaopr  13956  leexp2r  14091  hashf1lem1  14372  hashf1lem2  14373  ccatsymb  14500  wrd2ind  14640  cshweqrep  14738  rtrclreclem4  14978  lo1le  15569  summolem2  15633  summo  15634  prodmolem2  15852  prodmo  15853  bezoutlem3  16462  bezoutlem4  16463  qredeu  16579  pcadd  16811  prmreclem2  16839  vdwlem9  16911  vdwlem10  16912  ramub1lem2  16949  ramub1  16950  prmgaplem7  16979  cofucl  17805  initoeu2  17933  setcmon  18004  poslubmo  18325  posglbmo  18326  rabsubmgmd  18622  issubmd  18724  grprcan  18896  isnsg3  19082  ghmpreima  19160  gaorber  19230  psgneu  19428  odcau  19526  lsmsubm  19575  lsmmod  19597  ablfaclem3  20011  rngpropd  20102  ringpropd  20216  lmodvsmmulgdi  20840  lmodprop2d  20867  lss1d  20906  lindff1  21767  islindf4  21785  assamulgscmlem2  21847  mplcoe1  21982  mplcoe5  21985  evlslem1  22027  mdetunilem7  22543  mdetunilem8  22544  mdetunilem9  22545  mdetuni0  22546  mdetmul  22548  cayhamlem3  22812  ppttop  22932  epttop  22934  cnhaus  23279  isreg2  23302  cncmp  23317  1stcfb  23370  2ndcomap  23383  1stccnp  23387  cldllycmp  23420  1stckgenlem  23478  txcls  23529  ptcnp  23547  txdis1cn  23560  txlly  23561  txnlly  23562  pthaus  23563  txhaus  23572  txkgen  23577  xkohaus  23578  xkococnlem  23584  xkococn  23585  opnfbas  23767  hausflimi  23905  hausflim  23906  hauspwpwf1  23912  alexsubALT  23976  tgpconncomp  24038  qustgplem  24046  metequiv2  24435  met2ndci  24447  nrmmetd  24499  nlmvscnlem1  24611  reconn  24754  xrge0tsms  24760  mulc1cncf  24835  ipcnlem1  25182  minveclem3  25366  pmltpc  25388  ovolicc2lem5  25459  ovolicc2  25460  uniioombllem6  25526  dyadmbllem  25537  vitalilem3  25548  mbfmullem  25663  itg2split  25687  itg2mono  25691  bddiblnc  25780  dvlip2  25937  lhop1  25956  dvcnvrelem1  25959  dvfsumrlim  25975  ftc1lem6  25985  itgsubst  25993  dgrco  26218  plyexmo  26258  ulmdvlem3  26348  abelthlem2  26379  abelthlem8  26386  mpodvdsmulf1o  27141  dvdsmulf1o  27143  chpchtsum  27167  dchrptlem2  27213  2sqlem5  27370  2sqlem9  27375  2sqb  27380  chpo1ubb  27429  vmadivsumb  27431  selbergb  27497  selberg2b  27500  selberg3lem2  27506  pntrsumbnd  27514  pntrlog2bnd  27532  pntibndlem3  27540  pnt3  27560  noresle  27646  nosupprefixmo  27649  noinfprefixmo  27650  nosupbday  27654  noinfbday  27669  noinfbnd1lem5  27676  addsprop  27929  mulsproplem9  28073  mulsasslem3  28114  expadds  28368  readdscl  28411  tgjustf  28461  hlcgreu  28606  mirreu3  28642  cgraswap  28808  cgracom  28810  cgratr  28811  flatcgra  28812  acopyeu  28822  axsegcon  28916  ax5seglem9  28926  axeuclid  28952  axcontlem10  28962  axcontlem12  28964  wwlksnredwwlkn0  29885  n4cyclfrgr  30282  frgrnbnb  30284  numclwwlk1lem2fo  30349  ablo4  30541  smcnlem  30688  pjhthmo  31293  pjpjpre  31410  lnconi  32024  resf1o  32724  mgcoval  32978  xrge0tsmsd  33053  erlval  33236  derangenlem  35226  pconnconn  35286  connpconn  35290  cvmfolem  35334  cvmliftmolem2  35337  cvmliftmo  35339  cvmliftlem7  35346  cvmlift2lem10  35367  cvmlift3lem8  35381  linecgr  36136  btwnconn1lem8  36149  btwnconn1lem14  36155  btwnconn3  36158  brsegle  36163  segletr  36169  segleantisym  36170  outsideofeq  36185  linethru  36208  finminlem  36373  nn0prpwlem  36377  neibastop2lem  36415  weiunpo  36520  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  42701  prjspner1  42734  mzpcl1  42836  mzpcompact2lem  42858  diophin  42879  pell14qrmulcl  42970  pwssplit4  43196  hbtlem2  43231  iunrelexpuztr  43826  stoweidlem57  46169  stoweidlem61  46173  fourierdlem92  46310  euoreqb  47223  prproropf1olem3  47619  prproropf1olem4  47620  fpprwpprb  47854  cycldlenngric  48042  grimgrtri  48063  2zlidl  48354  lmodvsmdi  48493  2arwcat  49715