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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  fcof1  7306  mpo0  7516  fpr3g  8308  fprresex  8333  wfrlem17OLD  8363  eroveu  8849  boxriin  8977  undomOLD  9105  fofinf1o  9381  finsschain  9410  suppeqfsuppbi  9429  fsuppunbi  9439  marypha1lem  9483  wemapsolem  9600  wemapso  9601  wemapso2lem  9602  cantnf  9743  iunfictbso  10164  enfin2i  10371  ttukeylem7  10565  fpwwe2lem2  10682  fpwwe2lem8  10688  fpwwe2lem11  10691  fpwwelem  10695  distrlem4pr  11076  mulcmpblnr  11121  prsrlem1  11122  dedekind  11434  divdivdiv  11976  divmuleq  11980  divadddiv  11990  divsubdiv  11991  lediv12a  12169  xmullem  13307  xlemul1a  13331  seqcaopr  14070  leexp2r  14204  hashf1lem1  14485  hashf1lem1OLD  14486  hashf1lem2  14487  ccatsymb  14611  wrd2ind  14752  cshweqrep  14850  rtrclreclem4  15087  lo1le  15677  summolem2  15741  summo  15742  prodmolem2  15958  prodmo  15959  bezoutlem3  16563  bezoutlem4  16564  qredeu  16680  pcadd  16912  prmreclem2  16940  vdwlem9  17012  vdwlem10  17013  ramub1lem2  17050  ramub1  17051  prmgaplem7  17080  cofucl  17928  initoeu2  18059  setcmon  18130  poslubmo  18457  posglbmo  18458  rabsubmgmd  18718  issubmd  18817  grprcan  18989  isnsg3  19176  ghmpreima  19254  gaorber  19324  psgneu  19526  odcau  19624  lsmsubm  19673  lsmmod  19695  ablfaclem3  20109  rngpropd  20179  ringpropd  20289  lmodvsmmulgdi  20895  lmodprop2d  20922  lss1d  20962  lindff1  21840  islindf4  21858  assamulgscmlem2  21919  mplcoe1  22066  mplcoe5  22069  evlslem1  22119  mdetunilem7  22634  mdetunilem8  22635  mdetunilem9  22636  mdetuni0  22637  mdetmul  22639  cayhamlem3  22903  ppttop  23024  epttop  23026  cnhaus  23372  isreg2  23395  cncmp  23410  1stcfb  23463  2ndcomap  23476  1stccnp  23480  cldllycmp  23513  1stckgenlem  23571  txcls  23622  ptcnp  23640  txdis1cn  23653  txlly  23654  txnlly  23655  pthaus  23656  txhaus  23665  txkgen  23670  xkohaus  23671  xkococnlem  23677  xkococn  23678  opnfbas  23860  hausflimi  23998  hausflim  23999  hauspwpwf1  24005  alexsubALT  24069  tgpconncomp  24131  qustgplem  24139  metequiv2  24533  met2ndci  24545  nrmmetd  24597  nlmvscnlem1  24717  reconn  24858  xrge0tsms  24864  mulc1cncf  24939  ipcnlem1  25287  minveclem3  25471  pmltpc  25493  ovolicc2lem5  25564  ovolicc2  25565  uniioombllem6  25631  dyadmbllem  25642  vitalilem3  25653  mbfmullem  25769  itg2split  25793  itg2mono  25797  bddiblnc  25885  dvlip2  26042  lhop1  26061  dvcnvrelem1  26064  dvfsumrlim  26080  ftc1lem6  26090  itgsubst  26098  dgrco  26326  plyexmo  26364  ulmdvlem3  26454  abelthlem2  26485  abelthlem8  26492  mpodvdsmulf1o  27245  dvdsmulf1o  27247  chpchtsum  27271  dchrptlem2  27317  2sqlem5  27474  2sqlem9  27479  2sqb  27484  chpo1ubb  27533  vmadivsumb  27535  selbergb  27601  selberg2b  27604  selberg3lem2  27610  pntrsumbnd  27618  pntrlog2bnd  27636  pntibndlem3  27644  pnt3  27664  noresle  27750  nosupprefixmo  27753  noinfprefixmo  27754  nosupbday  27758  noinfbday  27773  noinfbnd1lem5  27780  addsprop  28013  mulsproplem9  28148  mulsasslem3  28189  readdscl  28373  tgjustf  28423  hlcgreu  28568  mirreu3  28604  cgraswap  28770  cgracom  28772  cgratr  28773  flatcgra  28774  acopyeu  28784  axsegcon  28884  ax5seglem9  28894  axeuclid  28920  axcontlem10  28930  axcontlem12  28932  wwlksnredwwlkn0  29853  n4cyclfrgr  30247  frgrnbnb  30249  numclwwlk1lem2fo  30314  ablo4  30506  smcnlem  30653  pjhthmo  31258  pjpjpre  31375  lnconi  31989  resf1o  32670  mgcoval  32885  xrge0tsmsd  32967  erlval  33157  derangenlem  35066  pconnconn  35126  connpconn  35130  cvmfolem  35174  cvmliftmolem2  35177  cvmliftmo  35179  cvmliftlem7  35186  cvmlift2lem10  35207  cvmlift3lem8  35221  linecgr  35972  btwnconn1lem8  35985  btwnconn1lem14  35991  btwnconn3  35994  brsegle  35999  segletr  36005  segleantisym  36006  outsideofeq  36021  linethru  36044  finminlem  36098  nn0prpwlem  36102  neibastop2lem  36140  mblfinlem3  37427  ftc1cnnc  37460  isbnd3  37552  cvlcvr1  39104  athgt  39222  4atlem12  39378  paddasslem12  39597  paddasslem13  39598  cdleme0cp  39980  cdleme42keg  40252  cdleme42mgN  40254  trlord  40335  cdlemg6c  40386  cdlemkid4  40700  dihopelvalcpre  41014  dihmeetlem1N  41056  dihglblem5apreN  41057  dihmeetlem4preN  41072  dihmeetlem6  41075  dihmeetlem10N  41082  dihmeetlem11N  41083  dihmeetlem13N  41085  dihjatcclem4  41187  fsuppssind  42337  prjspner1  42370  mzpcl1  42477  mzpcompact2lem  42499  diophin  42520  pell14qrmulcl  42611  pwssplit4  42841  hbtlem2  42876  iunrelexpuztr  43477  stoweidlem57  45768  stoweidlem61  45772  fourierdlem92  45909  euoreqb  46812  prproropf1olem3  47167  prproropf1olem4  47168  fpprwpprb  47402  grimgrtri  47609  2zlidl  47718  lmodvsmdi  47862