Theorem simprrr 805

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrr	|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )

Proof of Theorem simprrr

Step	Hyp	Ref	Expression
1		simpr 477	. 2 |- ( ( ch /\ th ) -> th )
2	1	ad2antll 765	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  prproe  4434  f1prex  6539  fliftfun  6562  grpridd  6874  wfrlem17  7431  mapdom2  8131  domunfican  8233  fofinf1o  8241  finsschain  8273  wemaplem3  8453  oemapvali  8581  iunfictbso  8937  enfin2i  9143  fin1a2s  9236  distrlem4pr  9848  mulcmpblnr  9892  prsrlem1  9893  addsrmo  9894  mulsrmo  9895  divdivdiv  10726  divsubdiv  10741  lediv12a  10916  xralrple  12036  seqcaopr  12838  leexp2r  12918  hashbclem  13236  wrd2ind  13477  cshwidxmod  13549  rtrclreclem4  13801  relexpindlem  13803  rtrclind  13805  rlimresb  14296  summo  14448  fsum2dlem  14501  prodmo  14666  fprod2dlem  14710  bezoutlem3  15258  bezoutlem4  15259  qredeu  15372  coprmproddvdslem  15376  pcqmul  15558  pcadd  15593  pockthg  15610  ramub1lem2  15731  cshwsdisj  15805  mreexexlem4d  16307  issubc3  16509  cofucl  16548  setcmon  16737  setcepi  16738  drsdirfi  16938  poslubmo  17146  posglbmo  17147  ghmpreima  17682  gaorber  17741  psgnunilem4  17917  psgneu  17926  odcau  18019  pgpssslw  18029  fislw  18040  lsmsubm  18068  efgsfo  18152  pgpfac1  18479  pgpfaclem2  18481  pgpfaclem3  18482  unitgrp  18667  islmodd  18869  lmodprop2d  18925  lsspropd  19017  lbsextlem4  19161  assapropd  19327  evlslem1  19515  mdetunilem8  20425  mdetmul  20429  ppttop  20811  epttop  20813  restbas  20962  iscnp4  21067  cnpco  21071  nrmsep  21161  regsep2  21180  ordthauslem  21187  1stcfb  21248  2ndcctbss  21258  2ndcdisj  21259  2ndcomap  21261  dis2ndc  21263  1stcelcls  21264  nlly2i  21279  islly2  21287  hausllycmp  21297  lly1stc  21299  comppfsc  21335  1stckgenlem  21356  ptbasin  21380  txcls  21407  ptcnp  21425  txlly  21439  txnlly  21440  txtube  21443  txcmplem1  21444  txcmplem2  21445  xkococnlem  21462  basqtop  21514  regr1lem  21542  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  reghmph  21596  nrmhmph  21597  filuni  21689  rnelfmlem  21756  fmufil  21763  fclscf  21829  fclsfnflim  21831  flimfnfcls  21832  uffclsflim  21835  cnpfcfi  21844  cnpfcf  21845  alexsublem  21848  alexsubALTlem3  21853  tgpconncompeqg  21915  ghmcnp  21918  qustgplem  21924  blssps  22229  blss  22230  blcld  22310  metequiv2  22315  met2ndci  22327  prdsxmslem2  22334  txmetcnp  22352  nlmvscnlem1  22490  xrge0tsms  22637  ipcnlem1  23044  iscmet3  23091  cmetss  23113  minveclem3  23200  pmltpc  23219  ovolscalem2  23282  ovolicc2lem5  23289  ovolicc2  23290  nulmbl2  23304  ioombl1  23330  uniioombllem6  23356  uniioombl  23357  vitalilem3  23379  i1faddlem  23460  mbfmullem  23492  itg2const2  23508  itg2split  23516  lhop2  23778  dvfsumrlim  23794  itgsubst  23812  plydivex  24052  plyexmo  24068  ulmbdd  24152  cxploglim  24704  dchrptlem2  24990  lgsquad2lem2  25110  2sqlem5  25147  dchrvmasumif  25192  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem3  25208  dchrisum0  25209  dchrmusum  25213  dchrvmasum  25214  pntibndlem3  25281  pntlemp  25299  ostth3  25327  legtrid  25486  hlcgreu  25513  mirreu3  25549  opphllem  25627  oppperpex  25645  lnperpex  25695  trgcopy  25696  iscgra1  25702  cgraswap  25712  cgracom  25714  cgratr  25715  acopyeu  25725  ax5seglem9  25817  ax5seg  25818  axcontlem8  25851  axcontlem12  25855  upgrclwlkcompim  26677  wlkwwlkfun  26781  wwlksnextwrd  26792  2pthfrgr  27148  frgrnbnb  27157  ablo4  27404  smcnlem  27552  pjhthmo  28161  1stpreimas  29483  xrge0tsmsd  29785  locfinref  29908  xpinpreima2  29953  qqhval2  30026  dya2iocnrect  30343  orvcgteel  30529  orvclteel  30534  cnpconn  31212  txpconn  31214  connpconn  31217  pconnpi1  31219  iccllysconn  31232  rellysconn  31233  cvmcov2  31257  cvmliftmolem2  31264  cvmliftmo  31266  cvmliftlem15  31280  cvmliftpht  31300  cvmlift3lem2  31302  nosupbnd1lem1  31854  nosupbnd2  31862  conway  31910  cgrextend  32115  btwnouttr2  32129  btwnexch2  32130  cgrxfr  32162  lineext  32183  btwnconn1lem5  32198  btwnconn1lem13  32206  btwnconn3  32210  segletr  32221  segleantisym  32222  outsideofeq  32237  outsidele  32239  lineunray  32254  refssfne  32353  neibastop2lem  32355  neibastop2  32356  unblimceq0lem  32497  knoppndvlem22  32524  mblfinlem3  33448  mblfinlem4  33449  cnambfre  33458  itg2addnclem  33461  areacirclem5  33504  istotbnd3  33570  crngm4  33802  cvlcvr1  34626  4atlem12  34898  cdlemb  35080  paddasslem10  35115  paddasslem12  35117  paddasslem13  35118  lhpexle3lem  35297  cdlemd4  35488  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme32d  35732  cdleme32f  35734  cdleme40m  35755  cdleme40n  35756  cdleme50trn2  35839  cdlemftr3  35853  cdlemm10N  36407  dihvalcqpre  36524  dihopelvalcpre  36537  dihmeetlem1N  36579  dihglblem5apreN  36580  dihmeetlem4preN  36595  dihjat1lem  36717  mapd0  36954  mapdh9a  37079  mzpmfp  37310  mzpcompact2lem  37314  diophin  37336  pellexlem3  37395  pellex  37399  pell14qrmulcl  37427  jm2.19lem3  37558  jm2.25  37566  jm2.27b  37573  fnwe2lem2  37621  hbtlem2  37694  hbtlem5  37698  gsumws3  38499  gsumws4  38500  fnchoice  39188  stoweidlem53  40270  stoweidlem61  40278  qndenserrnbllem  40514  bgoldbtbnd  41697