Theorem simprll 798

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 472	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrl 760	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  disjxiunOLD  4580  fcof1  6442  mpt20  6623  wfrlem17  7318  eroveu  7729  boxriin  7836  undom  7933  fofinf1o  8126  finsschain  8156  suppeqfsuppbi  8172  fsuppunbi  8179  marypha1lem  8222  wemapsolem  8338  wemapso  8339  wemapso2lem  8340  cantnf  8473  iunfictbso  8820  enfin2i  9026  ttukeylem7  9220  fpwwe2lem2  9333  fpwwe2lem9  9339  fpwwe2lem12  9342  fpwwelem  9346  distrlem4pr  9727  mulcmpblnr  9771  prsrlem1  9772  dedekind  10079  divdivdiv  10605  divmuleq  10609  divadddiv  10619  divsubdiv  10620  lediv12a  10795  xmullem  11966  xlemul1a  11990  seqcaopr  12700  leexp2r  12780  hashf1lem1  13096  hashf1lem2  13097  wrd2ind  13329  cshweqrep  13418  lo1le  14230  summolem2  14294  summo  14295  prodmolem2  14504  prodmo  14505  bezoutlem3  15096  bezoutlem4  15097  qredeu  15210  pcadd  15431  prmreclem2  15459  vdwlem9  15531  vdwlem10  15532  ramub1lem2  15569  ramub1  15570  prmgaplem7  15599  cofucl  16371  setcmon  16560  poslubmo  16969  posglbmo  16970  issubmd  17172  grprcan  17278  isnsg3  17451  ghmpreima  17505  gaorber  17564  psgneu  17749  odcau  17842  lsmsubm  17891  lsmmod  17911  ablfaclem3  18309  ringpropd  18405  lmodvsmmulgdi  18721  lmodprop2d  18748  lss1d  18784  assamulgscmlem2  19170  mplcoe1  19286  mplcoe5  19289  evlslem1  19336  lindff1  19978  islindf4  19996  mdetunilem7  20243  mdetunilem8  20244  mdetunilem9  20245  mdetuni0  20246  mdetmul  20248  cayhamlem3  20511  ppttop  20621  epttop  20623  cnhaus  20968  isreg2  20991  cncmp  21005  1stcfb  21058  2ndcomap  21071  1stccnp  21075  cldllycmp  21108  1stckgenlem  21166  txcls  21217  ptcnp  21235  txdis1cn  21248  txlly  21249  txnlly  21250  pthaus  21251  txhaus  21260  txkgen  21265  xkohaus  21266  xkococnlem  21272  xkococn  21273  opnfbas  21456  hausflimi  21594  hausflim  21595  hauspwpwf1  21601  alexsubALT  21665  tgpconcomp  21726  qustgplem  21734  metequiv2  22125  met2ndci  22137  nrmmetd  22189  nlmvscnlem1  22300  reconn  22439  xrge0tsms  22445  mulc1cncf  22516  ipcnlem1  22852  minveclem3  23008  pmltpc  23026  ovolicc2lem5  23096  ovolicc2  23097  uniioombllem6  23162  dyadmbllem  23173  vitalilem3  23185  mbfmullem  23298  itg2split  23322  itg2mono  23326  dvlip2  23562  lhop1  23581  dvcnvrelem1  23584  dvfsumrlim  23598  ftc1lem6  23608  itgsubst  23616  dgrco  23835  plyexmo  23872  ulmdvlem3  23960  abelthlem2  23990  abelthlem8  23997  dvdsmulf1o  24720  chpchtsum  24744  dchrptlem2  24790  2sqlem5  24947  2sqlem9  24952  2sqb  24957  chpo1ubb  24970  vmadivsumb  24972  selbergb  25038  selberg2b  25041  selberg3lem2  25047  pntrsumbnd  25055  pntrlog2bnd  25073  pntibndlem3  25081  pnt3  25101  hlcgreu  25313  mirreu3  25349  cgraswap  25512  cgracom  25514  cgratr  25515  acopyeu  25525  axsegcon  25607  ax5seglem9  25617  axeuclid  25643  axcontlem10  25653  axcontlem12  25655  wwlknredwwlkn0  26255  clwwlkextfrlem1  26603  numclwlk1lem2f1  26621  numclwlk1lem2fo  26622  ablo4  26788  smcnlem  26936  pjhthmo  27545  pjpjpre  27662  lnconi  28276  resf1o  28893  xrge0tsmsd  29116  derangenlem  30407  pconcon  30467  conpcon  30471  cvmfolem  30515  cvmliftmolem2  30518  cvmliftmo  30520  cvmliftlem7  30527  cvmlift2lem10  30548  cvmlift3lem8  30562  linecgr  31358  btwnconn1lem8  31371  btwnconn1lem14  31377  btwnconn3  31380  brsegle  31385  segletr  31391  segleantisym  31392  outsideofeq  31407  linethru  31430  finminlem  31482  nn0prpwlem  31487  neibastop2lem  31525  mblfinlem3  32618  bddiblnc  32650  ftc1cnnc  32654  isbnd3  32753  cvlcvr1  33644  athgt  33760  4atlem12  33916  paddasslem12  34135  paddasslem13  34136  cdleme0cp  34519  cdleme42keg  34792  cdleme42mgN  34794  trlord  34875  cdlemg6c  34926  cdlemkid4  35240  dihopelvalcpre  35555  dihmeetlem1N  35597  dihglblem5apreN  35598  dihmeetlem4preN  35613  dihmeetlem6  35616  dihmeetlem10N  35623  dihmeetlem11N  35624  dihmeetlem13N  35626  dihjatcclem4  35728  mzpcl1  36310  mzpcompact2lem  36332  diophin  36354  pell14qrmulcl  36445  pwssplit4  36677  hbtlem2  36713  iunrelexpuztr  37030  stoweidlem57  38950  stoweidlem61  38954  fourierdlem92  39091  wwlksnredwwlkn0  41102  frgrnbnb  41463  av-numclwlk1lem2f1  41524  av-numclwlk1lem2fo  41525  rabsubmgmd  41581  2zlidl  41724  lmodvsmdi  41957