Theorem simprrr 764

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  6196  grpridd  6497  mapdom2  7685  domunfican  7789  fofinf1o  7797  finsschain  7823  wemaplem3  7969  oemapvali  8099  iunfictbso  8491  enfin2i  8697  fin1a2s  8790  distrlem4pr  9400  mulcmpblnr  9444  prsrlem1  9445  addsrmo  9446  mulsrmo  9447  divdivdiv  10241  divsubdiv  10256  lediv12a  10434  xralrple  11400  seqcaopr  12108  leexp2r  12187  hashbclem  12463  wrd2ind  12662  cshwidxmod  12733  rlimresb  13347  summo  13498  fsum2dlem  13544  bezoutlem3  14033  bezoutlem4  14034  qredeu  14103  pcqmul  14232  pcadd  14263  pockthg  14279  ramub1lem2  14400  cshwsdisj  14437  mreexexlem4d  14898  issubc3  15072  cofucl  15111  setcmon  15268  setcepi  15269  drsdirfi  15421  poslubmo  15629  posglbmo  15630  ghmpreima  16083  gaorber  16141  psgnunilem4  16318  psgneu  16327  odcau  16420  pgpssslw  16430  fislw  16441  lsmsubm  16469  efgsfo  16553  pgpfac1  16921  pgpfaclem2  16923  pgpfaclem3  16924  unitgrp  17100  islmodd  17301  lmodprop2d  17355  lsspropd  17446  lbsextlem4  17590  assapropd  17747  evlslem1  17955  mdetunilem8  18888  mdetmul  18892  ppttop  19274  epttop  19276  restbas  19425  iscnp4  19530  cnpco  19534  nrmsep  19624  regsep2  19643  ordthauslem  19650  1stcfb  19712  2ndcctbss  19722  2ndcdisj  19723  2ndcomap  19725  dis2ndc  19727  1stcelcls  19728  nlly2i  19743  islly2  19751  hausllycmp  19761  lly1stc  19763  1stckgenlem  19789  ptbasin  19813  txcls  19840  ptcnp  19858  txlly  19872  txnlly  19873  txtube  19876  txcmplem1  19877  txcmplem2  19878  xkococnlem  19895  basqtop  19947  regr1lem  19975  kqreglem1  19977  kqreglem2  19978  kqnrmlem1  19979  kqnrmlem2  19980  reghmph  20029  nrmhmph  20030  filuni  20121  rnelfmlem  20188  fmufil  20195  fclscf  20261  fclsfnflim  20263  flimfnfcls  20264  uffclsflim  20267  cnpfcfi  20276  cnpfcf  20277  alexsublem  20279  alexsubALTlem3  20284  tgpconcompeqg  20345  ghmcnp  20348  divstgplem  20354  blssps  20662  blss  20663  blcld  20743  metequiv2  20748  met2ndci  20760  prdsxmslem2  20767  txmetcnp  20785  nlmvscnlem1  20930  xrge0tsms  21074  ipcnlem1  21420  iscmet3  21467  cmetss  21488  minveclem3  21579  pmltpc  21597  ovolscalem2  21660  ovolicc2lem5  21667  ovolicc2  21668  nulmbl2  21682  ioombl1  21707  uniioombllem6  21732  uniioombl  21733  vitalilem3  21754  i1faddlem  21835  mbfmullem  21867  itg2const2  21883  itg2split  21891  lhop2  22151  dvfsumrlim  22167  itgsubst  22185  plydivex  22427  plyexmo  22443  ulmbdd  22527  cxploglim  23035  dchrptlem2  23268  lgsquad2lem2  23362  2sqlem5  23371  dchrvmasumif  23416  rpvmasum2  23425  dchrisum0re  23426  dchrisum0lem3  23432  dchrisum0  23433  dchrmusum  23437  dchrvmasum  23438  pntibndlem3  23505  pntlemp  23523  ostth3  23551  legtrid  23705  mirreu3  23748  mideulem  23813  ax5seglem9  23916  ax5seg  23917  axcontlem8  23950  axcontlem12  23954  wlkiswwlkfun  24393  wwlkextwrd  24404  usg2spthonot0  24565  frgranbnb  24696  frgrancvvdeqlemC  24716  ablo4  24965  smcnlem  25283  pjhthmo  25896  xrge0tsmsd  27438  xpinpreima2  27525  qqhval2  27599  dya2iocnrect  27892  orvcgteel  28046  orvclteel  28051  cnpcon  28315  txpcon  28317  conpcon  28320  pconpi1  28322  iccllyscon  28335  rellyscon  28336  cvmcov2  28360  cvmliftmolem2  28367  cvmliftmo  28369  cvmliftlem15  28383  cvmliftpht  28403  cvmlift3lem2  28405  relexpsucl  28530  relexpcnv  28531  relexpdm  28533  relexprn  28534  relexpadd  28536  relexpindlem  28537  rtrclreclem.min  28545  rtrclind  28547  prodmo  28645  fprod2dlem  28687  cgrextend  29235  btwnouttr2  29249  btwnexch2  29250  cgrxfr  29282  lineext  29303  btwnconn1lem5  29318  btwnconn1lem13  29326  btwnconn3  29330  segletr  29341  segleantisym  29342  outsideofeq  29357  outsidele  29359  lineunray  29374  mblfinlem3  29630  mblfinlem4  29631  cnambfre  29640  itg2addnclem  29643  areacirclem5  29688  comppfsc  29779  neibastop2lem  29781  neibastop2  29782  istotbnd3  29870  crngm4  30003  mzpmfp  30283  mzpmfpOLD  30284  mzpcompact2lem  30288  diophin  30310  pellexlem3  30371  pellex  30375  pell14qrmulcl  30403  jm2.19lem3  30537  jm2.25  30545  jm2.27b  30552  fnwe2lem2  30601  hbtlem2  30677  hbtlem5  30681  fnchoice  30982  stoweidlem53  31353  stoweidlem61  31361  cvlcvr1  34136  4atlem12  34408  cdlemb  34590  paddasslem10  34625  paddasslem12  34627  paddasslem13  34628  lhpexle3lem  34807  cdlemd4  34997  cdlemefs32sn1aw  35210  cdleme43fsv1snlem  35216  cdleme32d  35240  cdleme32f  35242  cdleme40m  35263  cdleme40n  35264  cdleme50trn2  35347  cdlemftr3  35361  cdlemm10N  35915  dihvalcqpre  36032  dihopelvalcpre  36045  dihmeetlem1N  36087  dihglblem5apreN  36088  dihmeetlem4preN  36103  dihjat1lem  36225  mapd0  36462  mapdh9a  36587