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  7262  mpo0  7474  fpr3g  8264  fprresex  8289  eroveu  8785  boxriin  8913  fofinf1o  9283  finsschain  9310  suppeqfsuppbi  9330  fsuppunbi  9340  marypha1lem  9384  wemapsolem  9503  wemapso  9504  wemapso2lem  9505  cantnf  9646  iunfictbso  10067  enfin2i  10274  ttukeylem7  10468  fpwwe2lem2  10585  fpwwe2lem8  10591  fpwwe2lem11  10594  fpwwelem  10598  distrlem4pr  10979  mulcmpblnr  11024  prsrlem1  11025  dedekind  11337  divdivdiv  11883  divmuleq  11887  divadddiv  11897  divsubdiv  11898  lediv12a  12076  xmullem  13224  xlemul1a  13248  seqcaopr  14004  leexp2r  14139  hashf1lem1  14420  hashf1lem2  14421  ccatsymb  14547  wrd2ind  14688  cshweqrep  14786  rtrclreclem4  15027  lo1le  15618  summolem2  15682  summo  15683  prodmolem2  15901  prodmo  15902  bezoutlem3  16511  bezoutlem4  16512  qredeu  16628  pcadd  16860  prmreclem2  16888  vdwlem9  16960  vdwlem10  16961  ramub1lem2  16998  ramub1  16999  prmgaplem7  17028  cofucl  17850  initoeu2  17978  setcmon  18049  poslubmo  18370  posglbmo  18371  rabsubmgmd  18631  issubmd  18733  grprcan  18905  isnsg3  19092  ghmpreima  19170  gaorber  19240  psgneu  19436  odcau  19534  lsmsubm  19583  lsmmod  19605  ablfaclem3  20019  rngpropd  20083  ringpropd  20197  lmodvsmmulgdi  20803  lmodprop2d  20830  lss1d  20869  lindff1  21729  islindf4  21747  assamulgscmlem2  21809  mplcoe1  21944  mplcoe5  21947  evlslem1  21989  mdetunilem7  22505  mdetunilem8  22506  mdetunilem9  22507  mdetuni0  22508  mdetmul  22510  cayhamlem3  22774  ppttop  22894  epttop  22896  cnhaus  23241  isreg2  23264  cncmp  23279  1stcfb  23332  2ndcomap  23345  1stccnp  23349  cldllycmp  23382  1stckgenlem  23440  txcls  23491  ptcnp  23509  txdis1cn  23522  txlly  23523  txnlly  23524  pthaus  23525  txhaus  23534  txkgen  23539  xkohaus  23540  xkococnlem  23546  xkococn  23547  opnfbas  23729  hausflimi  23867  hausflim  23868  hauspwpwf1  23874  alexsubALT  23938  tgpconncomp  24000  qustgplem  24008  metequiv2  24398  met2ndci  24410  nrmmetd  24462  nlmvscnlem1  24574  reconn  24717  xrge0tsms  24723  mulc1cncf  24798  ipcnlem1  25145  minveclem3  25329  pmltpc  25351  ovolicc2lem5  25422  ovolicc2  25423  uniioombllem6  25489  dyadmbllem  25500  vitalilem3  25511  mbfmullem  25626  itg2split  25650  itg2mono  25654  bddiblnc  25743  dvlip2  25900  lhop1  25919  dvcnvrelem1  25922  dvfsumrlim  25938  ftc1lem6  25948  itgsubst  25956  dgrco  26181  plyexmo  26221  ulmdvlem3  26311  abelthlem2  26342  abelthlem8  26349  mpodvdsmulf1o  27104  dvdsmulf1o  27106  chpchtsum  27130  dchrptlem2  27176  2sqlem5  27333  2sqlem9  27338  2sqb  27343  chpo1ubb  27392  vmadivsumb  27394  selbergb  27460  selberg2b  27463  selberg3lem2  27469  pntrsumbnd  27477  pntrlog2bnd  27495  pntibndlem3  27503  pnt3  27523  noresle  27609  nosupprefixmo  27612  noinfprefixmo  27613  nosupbday  27617  noinfbday  27632  noinfbnd1lem5  27639  addsprop  27883  mulsproplem9  28027  mulsasslem3  28068  expadds  28320  readdscl  28350  tgjustf  28400  hlcgreu  28545  mirreu3  28581  cgraswap  28747  cgracom  28749  cgratr  28750  flatcgra  28751  acopyeu  28761  axsegcon  28854  ax5seglem9  28864  axeuclid  28890  axcontlem10  28900  axcontlem12  28902  wwlksnredwwlkn0  29826  n4cyclfrgr  30220  frgrnbnb  30222  numclwwlk1lem2fo  30287  ablo4  30479  smcnlem  30626  pjhthmo  31231  pjpjpre  31348  lnconi  31962  resf1o  32653  mgcoval  32912  xrge0tsmsd  33002  erlval  33209  derangenlem  35158  pconnconn  35218  connpconn  35222  cvmfolem  35266  cvmliftmolem2  35269  cvmliftmo  35271  cvmliftlem7  35278  cvmlift2lem10  35299  cvmlift3lem8  35313  linecgr  36069  btwnconn1lem8  36082  btwnconn1lem14  36088  btwnconn3  36091  brsegle  36096  segletr  36102  segleantisym  36103  outsideofeq  36118  linethru  36141  finminlem  36306  nn0prpwlem  36310  neibastop2lem  36348  weiunpo  36453  mblfinlem3  37653  ftc1cnnc  37686  isbnd3  37778  cvlcvr1  39332  athgt  39450  4atlem12  39606  paddasslem12  39825  paddasslem13  39826  cdleme0cp  40208  cdleme42keg  40480  cdleme42mgN  40482  trlord  40563  cdlemg6c  40614  cdlemkid4  40928  dihopelvalcpre  41242  dihmeetlem1N  41284  dihglblem5apreN  41285  dihmeetlem4preN  41300  dihmeetlem6  41303  dihmeetlem10N  41310  dihmeetlem11N  41311  dihmeetlem13N  41313  dihjatcclem4  41415  fsuppssind  42581  prjspner1  42614  mzpcl1  42717  mzpcompact2lem  42739  diophin  42760  pell14qrmulcl  42851  pwssplit4  43078  hbtlem2  43113  iunrelexpuztr  43708  stoweidlem57  46055  stoweidlem61  46059  fourierdlem92  46196  euoreqb  47110  prproropf1olem3  47506  prproropf1olem4  47507  fpprwpprb  47741  cycldlenngric  47928  grimgrtri  47948  2zlidl  48228  lmodvsmdi  48367  2arwcat  49589