Theorem simprrr 766

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 461	. 2 |- ( ( ch /\ th ) -> th )
2	1	ad2antll 728	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  fliftfun  6195  grpridd  6500  mapdom2  7690  domunfican  7795  fofinf1o  7803  finsschain  7829  wemaplem3  7976  oemapvali  8106  iunfictbso  8498  enfin2i  8704  fin1a2s  8797  distrlem4pr  9407  mulcmpblnr  9451  prsrlem1  9452  addsrmo  9453  mulsrmo  9454  divdivdiv  10252  divsubdiv  10267  lediv12a  10445  xralrple  11415  seqcaopr  12126  leexp2r  12205  hashbclem  12483  wrd2ind  12685  cshwidxmod  12756  rlimresb  13370  summo  13521  fsum2dlem  13567  prodmo  13725  fprod2dlem  13766  bezoutlem3  14160  bezoutlem4  14161  qredeu  14230  pcqmul  14359  pcadd  14390  pockthg  14406  ramub1lem2  14527  cshwsdisj  14565  mreexexlem4d  15026  issubc3  15197  cofucl  15236  setcmon  15393  setcepi  15394  drsdirfi  15546  poslubmo  15755  posglbmo  15756  ghmpreima  16267  gaorber  16325  psgnunilem4  16501  psgneu  16510  odcau  16603  pgpssslw  16613  fislw  16624  lsmsubm  16652  efgsfo  16736  pgpfac1  17110  pgpfaclem2  17112  pgpfaclem3  17113  unitgrp  17295  islmodd  17497  lmodprop2d  17551  lsspropd  17642  lbsextlem4  17786  assapropd  17955  evlslem1  18163  mdetunilem8  19099  mdetmul  19103  ppttop  19486  epttop  19488  restbas  19637  iscnp4  19742  cnpco  19746  nrmsep  19836  regsep2  19855  ordthauslem  19862  1stcfb  19924  2ndcctbss  19934  2ndcdisj  19935  2ndcomap  19937  dis2ndc  19939  1stcelcls  19940  nlly2i  19955  islly2  19963  hausllycmp  19973  lly1stc  19975  comppfsc  20011  1stckgenlem  20032  ptbasin  20056  txcls  20083  ptcnp  20101  txlly  20115  txnlly  20116  txtube  20119  txcmplem1  20120  txcmplem2  20121  xkococnlem  20138  basqtop  20190  regr1lem  20218  kqreglem1  20220  kqreglem2  20221  kqnrmlem1  20222  kqnrmlem2  20223  reghmph  20272  nrmhmph  20273  filuni  20364  rnelfmlem  20431  fmufil  20438  fclscf  20504  fclsfnflim  20506  flimfnfcls  20507  uffclsflim  20510  cnpfcfi  20519  cnpfcf  20520  alexsublem  20522  alexsubALTlem3  20527  tgpconcompeqg  20588  ghmcnp  20591  qustgplem  20597  blssps  20905  blss  20906  blcld  20986  metequiv2  20991  met2ndci  21003  prdsxmslem2  21010  txmetcnp  21028  nlmvscnlem1  21173  xrge0tsms  21317  ipcnlem1  21663  iscmet3  21710  cmetss  21731  minveclem3  21822  pmltpc  21840  ovolscalem2  21903  ovolicc2lem5  21910  ovolicc2  21911  nulmbl2  21925  ioombl1  21950  uniioombllem6  21975  uniioombl  21976  vitalilem3  21997  i1faddlem  22078  mbfmullem  22110  itg2const2  22126  itg2split  22134  lhop2  22394  dvfsumrlim  22410  itgsubst  22428  plydivex  22671  plyexmo  22687  ulmbdd  22771  cxploglim  23285  dchrptlem2  23518  lgsquad2lem2  23612  2sqlem5  23621  dchrvmasumif  23666  rpvmasum2  23675  dchrisum0re  23676  dchrisum0lem3  23682  dchrisum0  23683  dchrmusum  23687  dchrvmasum  23688  pntibndlem3  23755  pntlemp  23773  ostth3  23801  legtrid  23956  mirreu3  24013  opphllem  24087  ax5seglem9  24218  ax5seg  24219  axcontlem8  24252  axcontlem12  24256  wlkiswwlkfun  24695  wwlkextwrd  24706  usg2spthonot0  24867  frgranbnb  24998  frgrancvvdeqlemC  25017  ablo4  25267  smcnlem  25585  pjhthmo  26198  xrge0tsmsd  27753  locfinref  27822  xpinpreima2  27867  qqhval2  27941  dya2iocnrect  28230  orvcgteel  28384  orvclteel  28389  cnpcon  28653  txpcon  28655  conpcon  28658  pconpi1  28660  iccllyscon  28673  rellyscon  28674  cvmcov2  28698  cvmliftmolem2  28705  cvmliftmo  28707  cvmliftlem15  28721  cvmliftpht  28741  cvmlift3lem2  28743  relexpsucl  29033  relexpcnv  29034  relexpdm  29036  relexprn  29037  relexpadd  29039  relexpindlem  29040  rtrclreclem.min  29048  rtrclind  29050  cgrextend  29634  btwnouttr2  29648  btwnexch2  29649  cgrxfr  29681  lineext  29702  btwnconn1lem5  29717  btwnconn1lem13  29725  btwnconn3  29729  segletr  29740  segleantisym  29741  outsideofeq  29756  outsidele  29758  lineunray  29773  mblfinlem3  30029  mblfinlem4  30030  cnambfre  30039  itg2addnclem  30042  areacirclem5  30087  refssfne  30152  neibastop2lem  30154  neibastop2  30155  istotbnd3  30243  crngm4  30376  mzpmfp  30655  mzpmfpOLD  30656  mzpcompact2lem  30660  diophin  30682  pellexlem3  30743  pellex  30747  pell14qrmulcl  30775  jm2.19lem3  30909  jm2.25  30917  jm2.27b  30924  fnwe2lem2  30973  hbtlem2  31049  hbtlem5  31053  fnchoice  31358  stoweidlem53  31789  stoweidlem61  31797  cvlcvr1  34939  4atlem12  35211  cdlemb  35393  paddasslem10  35428  paddasslem12  35430  paddasslem13  35431  lhpexle3lem  35610  cdlemd4  35801  cdlemefs32sn1aw  36015  cdleme43fsv1snlem  36021  cdleme32d  36045  cdleme32f  36047  cdleme40m  36068  cdleme40n  36069  cdleme50trn2  36152  cdlemftr3  36166  cdlemm10N  36720  dihvalcqpre  36837  dihopelvalcpre  36850  dihmeetlem1N  36892  dihglblem5apreN  36893  dihmeetlem4preN  36908  dihjat1lem  37030  mapd0  37267  mapdh9a  37392