Theorem simprll 777

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  fcof1  7281  mpo0  7490  fpr3g  8266  fprresex  8291  wfrlem17OLD  8321  eroveu  8802  boxriin  8930  undomOLD  9056  fofinf1o  9323  finsschain  9355  suppeqfsuppbi  9373  fsuppunbi  9380  marypha1lem  9424  wemapsolem  9541  wemapso  9542  wemapso2lem  9543  cantnf  9684  iunfictbso  10105  enfin2i  10312  ttukeylem7  10506  fpwwe2lem2  10623  fpwwe2lem8  10629  fpwwe2lem11  10632  fpwwelem  10636  distrlem4pr  11017  mulcmpblnr  11062  prsrlem1  11063  dedekind  11373  divdivdiv  11911  divmuleq  11915  divadddiv  11925  divsubdiv  11926  lediv12a  12103  xmullem  13239  xlemul1a  13263  seqcaopr  14001  leexp2r  14135  hashf1lem1  14411  hashf1lem1OLD  14412  hashf1lem2  14413  ccatsymb  14528  wrd2ind  14669  cshweqrep  14767  rtrclreclem4  15004  lo1le  15594  summolem2  15658  summo  15659  prodmolem2  15875  prodmo  15876  bezoutlem3  16479  bezoutlem4  16480  qredeu  16591  pcadd  16818  prmreclem2  16846  vdwlem9  16918  vdwlem10  16919  ramub1lem2  16956  ramub1  16957  prmgaplem7  16986  cofucl  17834  initoeu2  17962  setcmon  18033  poslubmo  18360  posglbmo  18361  issubmd  18683  grprcan  18854  isnsg3  19034  ghmpreima  19108  gaorber  19166  psgneu  19368  odcau  19466  lsmsubm  19515  lsmmod  19537  ablfaclem3  19951  ringpropd  20095  lmodvsmmulgdi  20499  lmodprop2d  20526  lss1d  20566  lindff1  21366  islindf4  21384  assamulgscmlem2  21445  mplcoe1  21583  mplcoe5  21586  evlslem1  21636  mdetunilem7  22111  mdetunilem8  22112  mdetunilem9  22113  mdetuni0  22114  mdetmul  22116  cayhamlem3  22380  ppttop  22501  epttop  22503  cnhaus  22849  isreg2  22872  cncmp  22887  1stcfb  22940  2ndcomap  22953  1stccnp  22957  cldllycmp  22990  1stckgenlem  23048  txcls  23099  ptcnp  23117  txdis1cn  23130  txlly  23131  txnlly  23132  pthaus  23133  txhaus  23142  txkgen  23147  xkohaus  23148  xkococnlem  23154  xkococn  23155  opnfbas  23337  hausflimi  23475  hausflim  23476  hauspwpwf1  23482  alexsubALT  23546  tgpconncomp  23608  qustgplem  23616  metequiv2  24010  met2ndci  24022  nrmmetd  24074  nlmvscnlem1  24194  reconn  24335  xrge0tsms  24341  mulc1cncf  24412  ipcnlem1  24753  minveclem3  24937  pmltpc  24958  ovolicc2lem5  25029  ovolicc2  25030  uniioombllem6  25096  dyadmbllem  25107  vitalilem3  25118  mbfmullem  25234  itg2split  25258  itg2mono  25262  bddiblnc  25350  dvlip2  25503  lhop1  25522  dvcnvrelem1  25525  dvfsumrlim  25539  ftc1lem6  25549  itgsubst  25557  dgrco  25780  plyexmo  25817  ulmdvlem3  25905  abelthlem2  25935  abelthlem8  25942  dvdsmulf1o  26687  chpchtsum  26711  dchrptlem2  26757  2sqlem5  26914  2sqlem9  26919  2sqb  26924  chpo1ubb  26973  vmadivsumb  26975  selbergb  27041  selberg2b  27044  selberg3lem2  27050  pntrsumbnd  27058  pntrlog2bnd  27076  pntibndlem3  27084  pnt3  27104  noresle  27189  nosupprefixmo  27192  noinfprefixmo  27193  nosupbday  27197  noinfbday  27212  noinfbnd1lem5  27219  addsprop  27449  mulsproplem9  27569  mulsasslem3  27609  tgjustf  27713  hlcgreu  27858  mirreu3  27894  cgraswap  28060  cgracom  28062  cgratr  28063  flatcgra  28064  acopyeu  28074  axsegcon  28174  ax5seglem9  28184  axeuclid  28210  axcontlem10  28220  axcontlem12  28222  wwlksnredwwlkn0  29139  n4cyclfrgr  29533  frgrnbnb  29535  numclwwlk1lem2fo  29600  ablo4  29790  smcnlem  29937  pjhthmo  30542  pjpjpre  30659  lnconi  31273  resf1o  31942  mgcoval  32143  xrge0tsmsd  32196  derangenlem  34150  pconnconn  34210  connpconn  34214  cvmfolem  34258  cvmliftmolem2  34261  cvmliftmo  34263  cvmliftlem7  34270  cvmlift2lem10  34291  cvmlift3lem8  34305  linecgr  35041  btwnconn1lem8  35054  btwnconn1lem14  35060  btwnconn3  35063  brsegle  35068  segletr  35074  segleantisym  35075  outsideofeq  35090  linethru  35113  finminlem  35191  nn0prpwlem  35195  neibastop2lem  35233  mblfinlem3  36515  ftc1cnnc  36548  isbnd3  36640  cvlcvr1  38197  athgt  38315  4atlem12  38471  paddasslem12  38690  paddasslem13  38691  cdleme0cp  39073  cdleme42keg  39345  cdleme42mgN  39347  trlord  39428  cdlemg6c  39479  cdlemkid4  39793  dihopelvalcpre  40107  dihmeetlem1N  40149  dihglblem5apreN  40150  dihmeetlem4preN  40165  dihmeetlem6  40168  dihmeetlem10N  40175  dihmeetlem11N  40176  dihmeetlem13N  40178  dihjatcclem4  40280  fsuppssind  41162  prjspner1  41364  mzpcl1  41452  mzpcompact2lem  41474  diophin  41495  pell14qrmulcl  41586  pwssplit4  41816  hbtlem2  41851  iunrelexpuztr  42455  stoweidlem57  44759  stoweidlem61  44763  fourierdlem92  44900  euoreqb  45803  prproropf1olem3  46159  prproropf1olem4  46160  fpprwpprb  46394  rabsubmgmd  46547  rngpropd  46659  2zlidl  46785  lmodvsmdi  47011