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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fcof1  7043  mpo0  7239  wfrlem17  7971  eroveu  8392  boxriin  8504  undom  8605  fofinf1o  8799  finsschain  8831  suppeqfsuppbi  8847  fsuppunbi  8854  marypha1lem  8897  wemapsolem  9014  wemapso  9015  wemapso2lem  9016  cantnf  9156  iunfictbso  9540  enfin2i  9743  ttukeylem7  9937  fpwwe2lem2  10054  fpwwe2lem9  10060  fpwwe2lem12  10063  fpwwelem  10067  distrlem4pr  10448  mulcmpblnr  10493  prsrlem1  10494  dedekind  10803  divdivdiv  11341  divmuleq  11345  divadddiv  11355  divsubdiv  11356  lediv12a  11533  xmullem  12658  xlemul1a  12682  seqcaopr  13408  leexp2r  13539  hashf1lem1  13814  hashf1lem2  13815  ccatsymb  13936  wrd2ind  14085  cshweqrep  14183  lo1le  15008  summolem2  15073  summo  15074  prodmolem2  15289  prodmo  15290  bezoutlem3  15889  bezoutlem4  15890  qredeu  16002  pcadd  16225  prmreclem2  16253  vdwlem9  16325  vdwlem10  16326  ramub1lem2  16363  ramub1  16364  prmgaplem7  16393  cofucl  17158  initoeu2  17276  setcmon  17347  poslubmo  17756  posglbmo  17757  issubmd  17971  grprcan  18137  isnsg3  18312  ghmpreima  18380  gaorber  18438  psgneu  18634  odcau  18729  lsmsubm  18778  lsmmod  18801  ablfaclem3  19209  ringpropd  19332  lmodvsmmulgdi  19669  lmodprop2d  19696  lss1d  19735  assamulgscmlem2  20129  mplcoe1  20246  mplcoe5  20249  evlslem1  20295  lindff1  20964  islindf4  20982  mdetunilem7  21227  mdetunilem8  21228  mdetunilem9  21229  mdetuni0  21230  mdetmul  21232  cayhamlem3  21495  ppttop  21615  epttop  21617  cnhaus  21962  isreg2  21985  cncmp  22000  1stcfb  22053  2ndcomap  22066  1stccnp  22070  cldllycmp  22103  1stckgenlem  22161  txcls  22212  ptcnp  22230  txdis1cn  22243  txlly  22244  txnlly  22245  pthaus  22246  txhaus  22255  txkgen  22260  xkohaus  22261  xkococnlem  22267  xkococn  22268  opnfbas  22450  hausflimi  22588  hausflim  22589  hauspwpwf1  22595  alexsubALT  22659  tgpconncomp  22721  qustgplem  22729  metequiv2  23120  met2ndci  23132  nrmmetd  23184  nlmvscnlem1  23295  reconn  23436  xrge0tsms  23442  mulc1cncf  23513  ipcnlem1  23848  minveclem3  24032  pmltpc  24051  ovolicc2lem5  24122  ovolicc2  24123  uniioombllem6  24189  dyadmbllem  24200  vitalilem3  24211  mbfmullem  24326  itg2split  24350  itg2mono  24354  dvlip2  24592  lhop1  24611  dvcnvrelem1  24614  dvfsumrlim  24628  ftc1lem6  24638  itgsubst  24646  dgrco  24865  plyexmo  24902  ulmdvlem3  24990  abelthlem2  25020  abelthlem8  25027  dvdsmulf1o  25771  chpchtsum  25795  dchrptlem2  25841  2sqlem5  25998  2sqlem9  26003  2sqb  26008  chpo1ubb  26057  vmadivsumb  26059  selbergb  26125  selberg2b  26128  selberg3lem2  26134  pntrsumbnd  26142  pntrlog2bnd  26160  pntibndlem3  26168  pnt3  26188  tgjustf  26259  hlcgreu  26404  mirreu3  26440  cgraswap  26606  cgracom  26608  cgratr  26609  flatcgra  26610  acopyeu  26620  axsegcon  26713  ax5seglem9  26723  axeuclid  26749  axcontlem10  26759  axcontlem12  26761  wwlksnredwwlkn0  27674  n4cyclfrgr  28070  frgrnbnb  28072  numclwwlk1lem2fo  28137  ablo4  28327  smcnlem  28474  pjhthmo  29079  pjpjpre  29196  lnconi  29810  resf1o  30466  xrge0tsmsd  30692  derangenlem  32418  pconnconn  32478  connpconn  32482  cvmfolem  32526  cvmliftmolem2  32529  cvmliftmo  32531  cvmliftlem7  32538  cvmlift2lem10  32559  cvmlift3lem8  32573  fpr3g  33122  noresle  33200  linecgr  33542  btwnconn1lem8  33555  btwnconn1lem14  33561  btwnconn3  33564  brsegle  33569  segletr  33575  segleantisym  33576  outsideofeq  33591  linethru  33614  finminlem  33666  nn0prpwlem  33670  neibastop2lem  33708  mblfinlem3  34946  bddiblnc  34977  ftc1cnnc  34981  isbnd3  35077  cvlcvr1  36490  athgt  36607  4atlem12  36763  paddasslem12  36982  paddasslem13  36983  cdleme0cp  37365  cdleme42keg  37637  cdleme42mgN  37639  trlord  37720  cdlemg6c  37771  cdlemkid4  38085  dihopelvalcpre  38399  dihmeetlem1N  38441  dihglblem5apreN  38442  dihmeetlem4preN  38457  dihmeetlem6  38460  dihmeetlem10N  38467  dihmeetlem11N  38468  dihmeetlem13N  38470  dihjatcclem4  38572  mzpcl1  39346  mzpcompact2lem  39368  diophin  39389  pell14qrmulcl  39480  pwssplit4  39709  hbtlem2  39744  iunrelexpuztr  40084  stoweidlem57  42362  stoweidlem61  42366  fourierdlem92  42503  euoreqb  43328  prproropf1olem3  43687  prproropf1olem4  43688  fpprwpprb  43925  rabsubmgmd  44078  2zlidl  44225  lmodvsmdi  44450