Theorem simprll 779

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  7307  mpo0  7518  fpr3g  8310  fprresex  8335  wfrlem17OLD  8365  eroveu  8852  boxriin  8980  undomOLD  9100  fofinf1o  9372  finsschain  9399  suppeqfsuppbi  9419  fsuppunbi  9429  marypha1lem  9473  wemapsolem  9590  wemapso  9591  wemapso2lem  9592  cantnf  9733  iunfictbso  10154  enfin2i  10361  ttukeylem7  10555  fpwwe2lem2  10672  fpwwe2lem8  10678  fpwwe2lem11  10681  fpwwelem  10685  distrlem4pr  11066  mulcmpblnr  11111  prsrlem1  11112  dedekind  11424  divdivdiv  11968  divmuleq  11972  divadddiv  11982  divsubdiv  11983  lediv12a  12161  xmullem  13306  xlemul1a  13330  seqcaopr  14080  leexp2r  14214  hashf1lem1  14494  hashf1lem2  14495  ccatsymb  14620  wrd2ind  14761  cshweqrep  14859  rtrclreclem4  15100  lo1le  15688  summolem2  15752  summo  15753  prodmolem2  15971  prodmo  15972  bezoutlem3  16578  bezoutlem4  16579  qredeu  16695  pcadd  16927  prmreclem2  16955  vdwlem9  17027  vdwlem10  17028  ramub1lem2  17065  ramub1  17066  prmgaplem7  17095  cofucl  17933  initoeu2  18061  setcmon  18132  poslubmo  18456  posglbmo  18457  rabsubmgmd  18717  issubmd  18819  grprcan  18991  isnsg3  19178  ghmpreima  19256  gaorber  19326  psgneu  19524  odcau  19622  lsmsubm  19671  lsmmod  19693  ablfaclem3  20107  rngpropd  20171  ringpropd  20285  lmodvsmmulgdi  20895  lmodprop2d  20922  lss1d  20961  lindff1  21840  islindf4  21858  assamulgscmlem2  21920  mplcoe1  22055  mplcoe5  22058  evlslem1  22106  mdetunilem7  22624  mdetunilem8  22625  mdetunilem9  22626  mdetuni0  22627  mdetmul  22629  cayhamlem3  22893  ppttop  23014  epttop  23016  cnhaus  23362  isreg2  23385  cncmp  23400  1stcfb  23453  2ndcomap  23466  1stccnp  23470  cldllycmp  23503  1stckgenlem  23561  txcls  23612  ptcnp  23630  txdis1cn  23643  txlly  23644  txnlly  23645  pthaus  23646  txhaus  23655  txkgen  23660  xkohaus  23661  xkococnlem  23667  xkococn  23668  opnfbas  23850  hausflimi  23988  hausflim  23989  hauspwpwf1  23995  alexsubALT  24059  tgpconncomp  24121  qustgplem  24129  metequiv2  24523  met2ndci  24535  nrmmetd  24587  nlmvscnlem1  24707  reconn  24850  xrge0tsms  24856  mulc1cncf  24931  ipcnlem1  25279  minveclem3  25463  pmltpc  25485  ovolicc2lem5  25556  ovolicc2  25557  uniioombllem6  25623  dyadmbllem  25634  vitalilem3  25645  mbfmullem  25760  itg2split  25784  itg2mono  25788  bddiblnc  25877  dvlip2  26034  lhop1  26053  dvcnvrelem1  26056  dvfsumrlim  26072  ftc1lem6  26082  itgsubst  26090  dgrco  26315  plyexmo  26355  ulmdvlem3  26445  abelthlem2  26476  abelthlem8  26483  mpodvdsmulf1o  27237  dvdsmulf1o  27239  chpchtsum  27263  dchrptlem2  27309  2sqlem5  27466  2sqlem9  27471  2sqb  27476  chpo1ubb  27525  vmadivsumb  27527  selbergb  27593  selberg2b  27596  selberg3lem2  27602  pntrsumbnd  27610  pntrlog2bnd  27628  pntibndlem3  27636  pnt3  27656  noresle  27742  nosupprefixmo  27745  noinfprefixmo  27746  nosupbday  27750  noinfbday  27765  noinfbnd1lem5  27772  addsprop  28009  mulsproplem9  28150  mulsasslem3  28191  readdscl  28431  tgjustf  28481  hlcgreu  28626  mirreu3  28662  cgraswap  28828  cgracom  28830  cgratr  28831  flatcgra  28832  acopyeu  28842  axsegcon  28942  ax5seglem9  28952  axeuclid  28978  axcontlem10  28988  axcontlem12  28990  wwlksnredwwlkn0  29916  n4cyclfrgr  30310  frgrnbnb  30312  numclwwlk1lem2fo  30377  ablo4  30569  smcnlem  30716  pjhthmo  31321  pjpjpre  31438  lnconi  32052  resf1o  32741  mgcoval  32976  xrge0tsmsd  33065  erlval  33262  derangenlem  35176  pconnconn  35236  connpconn  35240  cvmfolem  35284  cvmliftmolem2  35287  cvmliftmo  35289  cvmliftlem7  35296  cvmlift2lem10  35317  cvmlift3lem8  35331  linecgr  36082  btwnconn1lem8  36095  btwnconn1lem14  36101  btwnconn3  36104  brsegle  36109  segletr  36115  segleantisym  36116  outsideofeq  36131  linethru  36154  finminlem  36319  nn0prpwlem  36323  neibastop2lem  36361  weiunpo  36466  mblfinlem3  37666  ftc1cnnc  37699  isbnd3  37791  cvlcvr1  39340  athgt  39458  4atlem12  39614  paddasslem12  39833  paddasslem13  39834  cdleme0cp  40216  cdleme42keg  40488  cdleme42mgN  40490  trlord  40571  cdlemg6c  40622  cdlemkid4  40936  dihopelvalcpre  41250  dihmeetlem1N  41292  dihglblem5apreN  41293  dihmeetlem4preN  41308  dihmeetlem6  41311  dihmeetlem10N  41318  dihmeetlem11N  41319  dihmeetlem13N  41321  dihjatcclem4  41423  fsuppssind  42603  prjspner1  42636  mzpcl1  42740  mzpcompact2lem  42762  diophin  42783  pell14qrmulcl  42874  pwssplit4  43101  hbtlem2  43136  iunrelexpuztr  43732  stoweidlem57  46072  stoweidlem61  46076  fourierdlem92  46213  euoreqb  47121  prproropf1olem3  47492  prproropf1olem4  47493  fpprwpprb  47727  grimgrtri  47916  2zlidl  48156  lmodvsmdi  48295