Theorem simprll 776

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 725	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  7209  mpo0  7414  fpr3g  8163  fprresex  8188  wfrlem17OLD  8218  eroveu  8664  boxriin  8791  undomOLD  8917  fofinf1o  9184  finsschain  9216  suppeqfsuppbi  9232  fsuppunbi  9239  marypha1lem  9282  wemapsolem  9399  wemapso  9400  wemapso2lem  9401  cantnf  9542  iunfictbso  9963  enfin2i  10170  ttukeylem7  10364  fpwwe2lem2  10481  fpwwe2lem8  10487  fpwwe2lem11  10490  fpwwelem  10494  distrlem4pr  10875  mulcmpblnr  10920  prsrlem1  10921  dedekind  11231  divdivdiv  11769  divmuleq  11773  divadddiv  11783  divsubdiv  11784  lediv12a  11961  xmullem  13091  xlemul1a  13115  seqcaopr  13853  leexp2r  13985  hashf1lem1  14260  hashf1lem1OLD  14261  hashf1lem2  14262  ccatsymb  14378  wrd2ind  14526  cshweqrep  14624  rtrclreclem4  14863  lo1le  15454  summolem2  15519  summo  15520  prodmolem2  15736  prodmo  15737  bezoutlem3  16340  bezoutlem4  16341  qredeu  16452  pcadd  16679  prmreclem2  16707  vdwlem9  16779  vdwlem10  16780  ramub1lem2  16817  ramub1  16818  prmgaplem7  16847  cofucl  17692  initoeu2  17820  setcmon  17891  poslubmo  18218  posglbmo  18219  issubmd  18534  grprcan  18701  isnsg3  18876  ghmpreima  18944  gaorber  19002  psgneu  19202  odcau  19297  lsmsubm  19346  lsmmod  19368  ablfaclem3  19777  ringpropd  19908  lmodvsmmulgdi  20256  lmodprop2d  20283  lss1d  20323  lindff1  21125  islindf4  21143  assamulgscmlem2  21202  mplcoe1  21336  mplcoe5  21339  evlslem1  21390  mdetunilem7  21865  mdetunilem8  21866  mdetunilem9  21867  mdetuni0  21868  mdetmul  21870  cayhamlem3  22134  ppttop  22255  epttop  22257  cnhaus  22603  isreg2  22626  cncmp  22641  1stcfb  22694  2ndcomap  22707  1stccnp  22711  cldllycmp  22744  1stckgenlem  22802  txcls  22853  ptcnp  22871  txdis1cn  22884  txlly  22885  txnlly  22886  pthaus  22887  txhaus  22896  txkgen  22901  xkohaus  22902  xkococnlem  22908  xkococn  22909  opnfbas  23091  hausflimi  23229  hausflim  23230  hauspwpwf1  23236  alexsubALT  23300  tgpconncomp  23362  qustgplem  23370  metequiv2  23764  met2ndci  23776  nrmmetd  23828  nlmvscnlem1  23948  reconn  24089  xrge0tsms  24095  mulc1cncf  24166  ipcnlem1  24507  minveclem3  24691  pmltpc  24712  ovolicc2lem5  24783  ovolicc2  24784  uniioombllem6  24850  dyadmbllem  24861  vitalilem3  24872  mbfmullem  24988  itg2split  25012  itg2mono  25016  bddiblnc  25104  dvlip2  25257  lhop1  25276  dvcnvrelem1  25279  dvfsumrlim  25293  ftc1lem6  25303  itgsubst  25311  dgrco  25534  plyexmo  25571  ulmdvlem3  25659  abelthlem2  25689  abelthlem8  25696  dvdsmulf1o  26441  chpchtsum  26465  dchrptlem2  26511  2sqlem5  26668  2sqlem9  26673  2sqb  26678  chpo1ubb  26727  vmadivsumb  26729  selbergb  26795  selberg2b  26798  selberg3lem2  26804  pntrsumbnd  26812  pntrlog2bnd  26830  pntibndlem3  26838  pnt3  26858  noresle  26943  nosupprefixmo  26946  noinfprefixmo  26947  nosupbday  26951  noinfbday  26966  noinfbnd1lem5  26973  tgjustf  27064  hlcgreu  27209  mirreu3  27245  cgraswap  27411  cgracom  27413  cgratr  27414  flatcgra  27415  acopyeu  27425  axsegcon  27525  ax5seglem9  27535  axeuclid  27561  axcontlem10  27571  axcontlem12  27573  wwlksnredwwlkn0  28490  n4cyclfrgr  28884  frgrnbnb  28886  numclwwlk1lem2fo  28951  ablo4  29141  smcnlem  29288  pjhthmo  29893  pjpjpre  30010  lnconi  30624  resf1o  31293  mgcoval  31492  xrge0tsmsd  31545  derangenlem  33373  pconnconn  33433  connpconn  33437  cvmfolem  33481  cvmliftmolem2  33484  cvmliftmo  33486  cvmliftlem7  33493  cvmlift2lem10  33514  cvmlift3lem8  33528  linecgr  34474  btwnconn1lem8  34487  btwnconn1lem14  34493  btwnconn3  34496  brsegle  34501  segletr  34507  segleantisym  34508  outsideofeq  34523  linethru  34546  finminlem  34598  nn0prpwlem  34602  neibastop2lem  34640  mblfinlem3  35914  ftc1cnnc  35947  isbnd3  36040  cvlcvr1  37599  athgt  37717  4atlem12  37873  paddasslem12  38092  paddasslem13  38093  cdleme0cp  38475  cdleme42keg  38747  cdleme42mgN  38749  trlord  38830  cdlemg6c  38881  cdlemkid4  39195  dihopelvalcpre  39509  dihmeetlem1N  39551  dihglblem5apreN  39552  dihmeetlem4preN  39567  dihmeetlem6  39570  dihmeetlem10N  39577  dihmeetlem11N  39578  dihmeetlem13N  39580  dihjatcclem4  39682  fsuppssind  40532  prjspner1  40713  mzpcl1  40801  mzpcompact2lem  40823  diophin  40844  pell14qrmulcl  40935  pwssplit4  41165  hbtlem2  41200  iunrelexpuztr  41637  stoweidlem57  43923  stoweidlem61  43927  fourierdlem92  44064  euoreqb  44941  prproropf1olem3  45297  prproropf1olem4  45298  fpprwpprb  45532  rabsubmgmd  45685  2zlidl  45832  lmodvsmdi  46058