Theorem simprll 779

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 729	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  7233  mpo0  7443  fpr3g  8226  fprresex  8251  eroveu  8750  boxriin  8879  fofinf1o  9233  finsschain  9260  suppeqfsuppbi  9283  fsuppunbi  9293  marypha1lem  9337  wemapsolem  9456  wemapso  9457  wemapso2lem  9458  cantnf  9603  iunfictbso  10025  enfin2i  10232  ttukeylem7  10426  fpwwe2lem2  10544  fpwwe2lem8  10550  fpwwe2lem11  10553  fpwwelem  10557  distrlem4pr  10938  mulcmpblnr  10983  prsrlem1  10984  dedekind  11298  divdivdiv  11845  divmuleq  11849  divadddiv  11859  divsubdiv  11860  lediv12a  12038  xmullem  13205  xlemul1a  13229  seqcaopr  13990  leexp2r  14125  hashf1lem1  14406  hashf1lem2  14407  ccatsymb  14534  wrd2ind  14674  cshweqrep  14772  rtrclreclem4  15012  lo1le  15603  summolem2  15667  summo  15668  prodmolem2  15889  prodmo  15890  bezoutlem3  16499  bezoutlem4  16500  qredeu  16616  pcadd  16849  prmreclem2  16877  vdwlem9  16949  vdwlem10  16950  ramub1lem2  16987  ramub1  16988  prmgaplem7  17017  cofucl  17844  initoeu2  17972  setcmon  18043  poslubmo  18364  posglbmo  18365  rabsubmgmd  18661  issubmd  18763  grprcan  18938  isnsg3  19124  ghmpreima  19202  gaorber  19272  psgneu  19470  odcau  19568  lsmsubm  19617  lsmmod  19639  ablfaclem3  20053  rngpropd  20144  ringpropd  20258  lmodvsmmulgdi  20881  lmodprop2d  20908  lss1d  20947  lindff1  21808  islindf4  21826  assamulgscmlem2  21888  mplcoe1  22024  mplcoe5  22027  evlslem1  22069  mdetunilem7  22592  mdetunilem8  22593  mdetunilem9  22594  mdetuni0  22595  mdetmul  22597  cayhamlem3  22861  ppttop  22981  epttop  22983  cnhaus  23328  isreg2  23351  cncmp  23366  1stcfb  23419  2ndcomap  23432  1stccnp  23436  cldllycmp  23469  1stckgenlem  23527  txcls  23578  ptcnp  23596  txdis1cn  23609  txlly  23610  txnlly  23611  pthaus  23612  txhaus  23621  txkgen  23626  xkohaus  23627  xkococnlem  23633  xkococn  23634  opnfbas  23816  hausflimi  23954  hausflim  23955  hauspwpwf1  23961  alexsubALT  24025  tgpconncomp  24087  qustgplem  24095  metequiv2  24484  met2ndci  24496  nrmmetd  24548  nlmvscnlem1  24660  reconn  24803  xrge0tsms  24809  mulc1cncf  24881  ipcnlem1  25221  minveclem3  25405  pmltpc  25426  ovolicc2lem5  25497  ovolicc2  25498  uniioombllem6  25564  dyadmbllem  25575  vitalilem3  25586  mbfmullem  25701  itg2split  25725  itg2mono  25729  bddiblnc  25818  dvlip2  25972  lhop1  25991  dvcnvrelem1  25994  dvfsumrlim  26010  ftc1lem6  26020  itgsubst  26028  dgrco  26252  plyexmo  26292  ulmdvlem3  26382  abelthlem2  26413  abelthlem8  26420  mpodvdsmulf1o  27175  dvdsmulf1o  27177  chpchtsum  27201  dchrptlem2  27247  2sqlem5  27404  2sqlem9  27409  2sqb  27414  chpo1ubb  27463  vmadivsumb  27465  selbergb  27531  selberg2b  27534  selberg3lem2  27540  pntrsumbnd  27548  pntrlog2bnd  27566  pntibndlem3  27574  pnt3  27594  noresle  27680  nosupprefixmo  27683  noinfprefixmo  27684  nosupbday  27688  noinfbday  27703  noinfbnd1lem5  27710  addsprop  27987  mulsproplem9  28135  mulsasslem3  28176  expadds  28446  bdayfinbndlem1  28478  readdscl  28510  tgjustf  28560  hlcgreu  28705  mirreu3  28741  cgraswap  28907  cgracom  28909  cgratr  28910  flatcgra  28911  acopyeu  28921  axsegcon  29015  ax5seglem9  29025  axeuclid  29051  axcontlem10  29061  axcontlem12  29063  wwlksnredwwlkn0  29984  n4cyclfrgr  30381  frgrnbnb  30383  numclwwlk1lem2fo  30448  ablo4  30641  smcnlem  30788  pjhthmo  31393  pjpjpre  31510  lnconi  32124  resf1o  32823  mgcoval  33066  xrge0tsmsd  33154  erlval  33339  derangenlem  35374  pconnconn  35434  connpconn  35438  cvmfolem  35482  cvmliftmolem2  35485  cvmliftmo  35487  cvmliftlem7  35494  cvmlift2lem10  35515  cvmlift3lem8  35529  linecgr  36284  btwnconn1lem8  36297  btwnconn1lem14  36303  btwnconn3  36306  brsegle  36311  segletr  36317  segleantisym  36318  outsideofeq  36333  linethru  36356  finminlem  36521  nn0prpwlem  36525  neibastop2lem  36563  weiunpo  36668  mblfinlem3  37991  ftc1cnnc  38024  isbnd3  38116  cvlcvr1  39796  athgt  39913  4atlem12  40069  paddasslem12  40288  paddasslem13  40289  cdleme0cp  40671  cdleme42keg  40943  cdleme42mgN  40945  trlord  41026  cdlemg6c  41077  cdlemkid4  41391  dihopelvalcpre  41705  dihmeetlem1N  41747  dihglblem5apreN  41748  dihmeetlem4preN  41763  dihmeetlem6  41766  dihmeetlem10N  41773  dihmeetlem11N  41774  dihmeetlem13N  41776  dihjatcclem4  41878  fsuppssind  43037  prjspner1  43070  mzpcl1  43172  mzpcompact2lem  43194  diophin  43215  pell14qrmulcl  43306  pwssplit4  43532  hbtlem2  43567  iunrelexpuztr  44161  stoweidlem57  46500  stoweidlem61  46504  fourierdlem92  46641  euoreqb  47554  prproropf1olem3  47962  prproropf1olem4  47963  fpprwpprb  48213  cycldlenngric  48401  grimgrtri  48422  2zlidl  48713  lmodvsmdi  48852  2arwcat  50072