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 729	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  7243  mpo0  7453  fpr3g  8237  fprresex  8262  eroveu  8761  boxriin  8890  fofinf1o  9244  finsschain  9271  suppeqfsuppbi  9294  fsuppunbi  9304  marypha1lem  9348  wemapsolem  9467  wemapso  9468  wemapso2lem  9469  cantnf  9614  iunfictbso  10036  enfin2i  10243  ttukeylem7  10437  fpwwe2lem2  10555  fpwwe2lem8  10561  fpwwe2lem11  10564  fpwwelem  10568  distrlem4pr  10949  mulcmpblnr  10994  prsrlem1  10995  dedekind  11308  divdivdiv  11854  divmuleq  11858  divadddiv  11868  divsubdiv  11869  lediv12a  12047  xmullem  13191  xlemul1a  13215  seqcaopr  13974  leexp2r  14109  hashf1lem1  14390  hashf1lem2  14391  ccatsymb  14518  wrd2ind  14658  cshweqrep  14756  rtrclreclem4  14996  lo1le  15587  summolem2  15651  summo  15652  prodmolem2  15870  prodmo  15871  bezoutlem3  16480  bezoutlem4  16481  qredeu  16597  pcadd  16829  prmreclem2  16857  vdwlem9  16929  vdwlem10  16930  ramub1lem2  16967  ramub1  16968  prmgaplem7  16997  cofucl  17824  initoeu2  17952  setcmon  18023  poslubmo  18344  posglbmo  18345  rabsubmgmd  18641  issubmd  18743  grprcan  18915  isnsg3  19101  ghmpreima  19179  gaorber  19249  psgneu  19447  odcau  19545  lsmsubm  19594  lsmmod  19616  ablfaclem3  20030  rngpropd  20121  ringpropd  20235  lmodvsmmulgdi  20860  lmodprop2d  20887  lss1d  20926  lindff1  21787  islindf4  21805  assamulgscmlem2  21868  mplcoe1  22004  mplcoe5  22007  evlslem1  22049  mdetunilem7  22574  mdetunilem8  22575  mdetunilem9  22576  mdetuni0  22577  mdetmul  22579  cayhamlem3  22843  ppttop  22963  epttop  22965  cnhaus  23310  isreg2  23333  cncmp  23348  1stcfb  23401  2ndcomap  23414  1stccnp  23418  cldllycmp  23451  1stckgenlem  23509  txcls  23560  ptcnp  23578  txdis1cn  23591  txlly  23592  txnlly  23593  pthaus  23594  txhaus  23603  txkgen  23608  xkohaus  23609  xkococnlem  23615  xkococn  23616  opnfbas  23798  hausflimi  23936  hausflim  23937  hauspwpwf1  23943  alexsubALT  24007  tgpconncomp  24069  qustgplem  24077  metequiv2  24466  met2ndci  24478  nrmmetd  24530  nlmvscnlem1  24642  reconn  24785  xrge0tsms  24791  mulc1cncf  24866  ipcnlem1  25213  minveclem3  25397  pmltpc  25419  ovolicc2lem5  25490  ovolicc2  25491  uniioombllem6  25557  dyadmbllem  25568  vitalilem3  25579  mbfmullem  25694  itg2split  25718  itg2mono  25722  bddiblnc  25811  dvlip2  25968  lhop1  25987  dvcnvrelem1  25990  dvfsumrlim  26006  ftc1lem6  26016  itgsubst  26024  dgrco  26249  plyexmo  26289  ulmdvlem3  26379  abelthlem2  26410  abelthlem8  26417  mpodvdsmulf1o  27172  dvdsmulf1o  27174  chpchtsum  27198  dchrptlem2  27244  2sqlem5  27401  2sqlem9  27406  2sqb  27411  chpo1ubb  27460  vmadivsumb  27462  selbergb  27528  selberg2b  27531  selberg3lem2  27537  pntrsumbnd  27545  pntrlog2bnd  27563  pntibndlem3  27571  pnt3  27591  noresle  27677  nosupprefixmo  27680  noinfprefixmo  27681  nosupbday  27685  noinfbday  27700  noinfbnd1lem5  27707  addsprop  27984  mulsproplem9  28132  mulsasslem3  28173  expadds  28443  bdayfinbndlem1  28475  readdscl  28507  tgjustf  28557  hlcgreu  28702  mirreu3  28738  cgraswap  28904  cgracom  28906  cgratr  28907  flatcgra  28908  acopyeu  28918  axsegcon  29012  ax5seglem9  29022  axeuclid  29048  axcontlem10  29058  axcontlem12  29060  wwlksnredwwlkn0  29981  n4cyclfrgr  30378  frgrnbnb  30380  numclwwlk1lem2fo  30445  ablo4  30637  smcnlem  30784  pjhthmo  31389  pjpjpre  31506  lnconi  32120  resf1o  32819  mgcoval  33078  xrge0tsmsd  33166  erlval  33351  derangenlem  35384  pconnconn  35444  connpconn  35448  cvmfolem  35492  cvmliftmolem2  35495  cvmliftmo  35497  cvmliftlem7  35504  cvmlift2lem10  35525  cvmlift3lem8  35539  linecgr  36294  btwnconn1lem8  36307  btwnconn1lem14  36313  btwnconn3  36316  brsegle  36321  segletr  36327  segleantisym  36328  outsideofeq  36343  linethru  36366  finminlem  36531  nn0prpwlem  36535  neibastop2lem  36573  weiunpo  36678  mblfinlem3  37899  ftc1cnnc  37932  isbnd3  38024  cvlcvr1  39704  athgt  39821  4atlem12  39977  paddasslem12  40196  paddasslem13  40197  cdleme0cp  40579  cdleme42keg  40851  cdleme42mgN  40853  trlord  40934  cdlemg6c  40985  cdlemkid4  41299  dihopelvalcpre  41613  dihmeetlem1N  41655  dihglblem5apreN  41656  dihmeetlem4preN  41671  dihmeetlem6  41674  dihmeetlem10N  41681  dihmeetlem11N  41682  dihmeetlem13N  41684  dihjatcclem4  41786  fsuppssind  42940  prjspner1  42973  mzpcl1  43075  mzpcompact2lem  43097  diophin  43118  pell14qrmulcl  43209  pwssplit4  43435  hbtlem2  43470  iunrelexpuztr  44064  stoweidlem57  46404  stoweidlem61  46408  fourierdlem92  46545  euoreqb  47458  prproropf1olem3  47854  prproropf1olem4  47855  fpprwpprb  48089  cycldlenngric  48277  grimgrtri  48298  2zlidl  48589  lmodvsmdi  48728  2arwcat  49948