Theorem simprrr 775

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

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  f1prex  6182  fliftfun  6205  grpridd  6509  wfrlem17  7052  mapdom2  7743  domunfican  7844  fofinf1o  7852  finsschain  7881  wemaplem3  8063  oemapvali  8189  iunfictbso  8545  enfin2i  8751  fin1a2s  8844  distrlem4pr  9451  mulcmpblnr  9495  prsrlem1  9496  addsrmo  9497  mulsrmo  9498  divdivdiv  10308  divsubdiv  10323  lediv12a  10499  xralrple  11498  seqcaopr  12250  leexp2r  12330  hashbclem  12615  wrd2ind  12834  cshwidxmod  12905  rtrclreclem4  13124  relexpindlem  13126  rtrclind  13128  rlimresb  13629  summo  13783  fsum2dlem  13831  prodmo  13990  fprod2dlem  14034  bezoutlem3OLD  14505  bezoutlem4OLD  14506  bezoutlem3  14508  bezoutlem4  14509  qredeu  14664  coprmproddvdslem  14679  pcqmul  14803  pcadd  14834  pockthg  14850  ramub1lem2  14985  cshwsdisj  15069  mreexexlem4d  15553  issubc3  15754  cofucl  15793  setcmon  15982  setcepi  15983  drsdirfi  16183  poslubmo  16392  posglbmo  16393  ghmpreima  16904  gaorber  16962  psgnunilem4  17138  psgneu  17147  odcau  17256  pgpssslw  17266  fislw  17277  lsmsubm  17305  efgsfo  17389  pgpfac1  17713  pgpfaclem2  17715  pgpfaclem3  17716  unitgrp  17895  islmodd  18097  lmodprop2d  18150  lsspropd  18240  lbsextlem4  18384  assapropd  18551  evlslem1  18738  mdetunilem8  19644  mdetmul  19648  ppttop  20022  epttop  20024  restbas  20174  iscnp4  20279  cnpco  20283  nrmsep  20373  regsep2  20392  ordthauslem  20399  1stcfb  20460  2ndcctbss  20470  2ndcdisj  20471  2ndcomap  20473  dis2ndc  20475  1stcelcls  20476  nlly2i  20491  islly2  20499  hausllycmp  20509  lly1stc  20511  comppfsc  20547  1stckgenlem  20568  ptbasin  20592  txcls  20619  ptcnp  20637  txlly  20651  txnlly  20652  txtube  20655  txcmplem1  20656  txcmplem2  20657  xkococnlem  20674  basqtop  20726  regr1lem  20754  kqreglem1  20756  kqreglem2  20757  kqnrmlem1  20758  kqnrmlem2  20759  reghmph  20808  nrmhmph  20809  filuni  20900  rnelfmlem  20967  fmufil  20974  fclscf  21040  fclsfnflim  21042  flimfnfcls  21043  uffclsflim  21046  cnpfcfi  21055  cnpfcf  21056  alexsublem  21059  alexsubALTlem3  21064  tgpconcompeqg  21126  ghmcnp  21129  qustgplem  21135  blssps  21439  blss  21440  blcld  21520  metequiv2  21525  met2ndci  21537  prdsxmslem2  21544  txmetcnp  21562  nlmvscnlem1  21689  xrge0tsms  21852  ipcnlem1  22216  iscmet3  22263  cmetss  22284  minveclem3  22371  minveclem3OLD  22383  pmltpc  22401  ovolscalem2  22467  ovolicc2lem5  22475  ovolicc2  22476  nulmbl2  22490  ioombl1  22515  uniioombllem6  22546  uniioombl  22547  vitalilem3  22568  i1faddlem  22651  mbfmullem  22683  itg2const2  22699  itg2split  22707  lhop2  22967  dvfsumrlim  22983  itgsubst  23001  plydivex  23250  plyexmo  23266  ulmbdd  23353  cxploglim  23903  dchrptlem2  24193  lgsquad2lem2  24287  2sqlem5  24296  dchrvmasumif  24341  rpvmasum2  24350  dchrisum0re  24351  dchrisum0lem3  24357  dchrisum0  24358  dchrmusum  24362  dchrvmasum  24363  pntibndlem3  24430  pntlemp  24448  ostth3  24476  legtrid  24636  hlcgreu  24663  mirreu3  24699  opphllem  24777  oppperpex  24795  lnperpex  24845  trgcopy  24846  iscgra1  24852  cgraswap  24862  cgracom  24864  cgratr  24865  acopyeu  24875  ax5seglem9  24967  ax5seg  24968  axcontlem8  25001  axcontlem12  25005  wlkiswwlkfun  25445  wwlkextwrd  25456  usg2spthonot0  25617  frgranbnb  25748  frgrancvvdeqlemC  25767  ablo4  26015  smcnlem  26333  pjhthmo  26955  1stpreimas  28286  xrge0tsmsd  28548  locfinref  28668  xpinpreima2  28713  qqhval2  28786  dya2iocnrect  29103  orvcgteel  29300  orvclteel  29305  cnpcon  29953  txpcon  29955  conpcon  29958  pconpi1  29960  iccllyscon  29973  rellyscon  29974  cvmcov2  29998  cvmliftmolem2  30005  cvmliftmo  30007  cvmliftlem15  30021  cvmliftpht  30041  cvmlift3lem2  30043  cgrextend  30775  btwnouttr2  30789  btwnexch2  30790  cgrxfr  30822  lineext  30843  btwnconn1lem5  30858  btwnconn1lem13  30866  btwnconn3  30870  segletr  30881  segleantisym  30882  outsideofeq  30897  outsidele  30899  lineunray  30914  refssfne  31014  neibastop2lem  31016  neibastop2  31017  mblfinlem3  31979  mblfinlem4  31980  cnambfre  31989  itg2addnclem  31993  areacirclem5  32036  istotbnd3  32103  crngm4  32236  cvlcvr1  32905  4atlem12  33177  cdlemb  33359  paddasslem10  33394  paddasslem12  33396  paddasslem13  33397  lhpexle3lem  33576  cdlemd4  33767  cdlemefs32sn1aw  33981  cdleme43fsv1snlem  33987  cdleme32d  34011  cdleme32f  34013  cdleme40m  34034  cdleme40n  34035  cdleme50trn2  34118  cdlemftr3  34132  cdlemm10N  34686  dihvalcqpre  34803  dihopelvalcpre  34816  dihmeetlem1N  34858  dihglblem5apreN  34859  dihmeetlem4preN  34874  dihjat1lem  34996  mapd0  35233  mapdh9a  35358  mzpmfp  35589  mzpcompact2lem  35593  diophin  35615  pellexlem3  35675  pellex  35679  pell14qrmulcl  35709  jm2.19lem3  35846  jm2.25  35854  jm2.27b  35861  fnwe2lem2  35909  hbtlem2  35983  hbtlem5  35987  gsumws3  36648  gsumws4  36649  fnchoice  37350  stoweidlem53  37914  stoweidlem61  37922  qndenserrnbllem  38163  bgoldbtbnd  38904