Theorem simprrr 759

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 458	. 2 |- ( ( ch /\ th ) -> th )
2	1	ad2antll 723	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  6002  grpridd  6302  mapdom2  7478  domunfican  7580  fofinf1o  7588  finsschain  7614  wemaplem3  7758  oemapvali  7888  iunfictbso  8280  enfin2i  8486  fin1a2s  8579  distrlem4pr  9191  divdivdiv  10028  divsubdiv  10043  lediv12a  10221  xralrple  11171  seqcaopr  11839  leexp2r  11917  hashbclem  12201  wrd2ind  12368  cshwidxmod  12436  rlimresb  13039  summo  13190  fsum2dlem  13233  bezoutlem3  13720  bezoutlem4  13721  qredeu  13789  pcqmul  13916  pcadd  13947  pockthg  13963  ramub1lem2  14084  cshwsdisj  14121  mreexexlem4d  14581  issubc3  14755  cofucl  14794  setcmon  14951  setcepi  14952  drsdirfi  15104  poslubmo  15312  posglbmo  15313  ghmpreima  15761  gaorber  15819  psgnunilem4  15996  psgneu  16005  odcau  16096  pgpssslw  16106  fislw  16117  lsmsubm  16145  efgsfo  16229  pgpfac1  16571  pgpfaclem2  16573  pgpfaclem3  16574  unitgrp  16749  islmodd  16934  lmodprop2d  16987  lsspropd  17076  lbsextlem4  17220  assapropd  17376  evlslem1  17577  mdetunilem8  18384  mdetmul  18388  ppttop  18570  epttop  18572  restbas  18721  iscnp4  18826  cnpco  18830  nrmsep  18920  regsep2  18939  ordthauslem  18946  1stcfb  19008  2ndcctbss  19018  2ndcdisj  19019  2ndcomap  19021  dis2ndc  19023  1stcelcls  19024  nlly2i  19039  islly2  19047  hausllycmp  19057  lly1stc  19059  1stckgenlem  19085  ptbasin  19109  txcls  19136  ptcnp  19154  txlly  19168  txnlly  19169  txtube  19172  txcmplem1  19173  txcmplem2  19174  xkococnlem  19191  basqtop  19243  regr1lem  19271  kqreglem1  19273  kqreglem2  19274  kqnrmlem1  19275  kqnrmlem2  19276  reghmph  19325  nrmhmph  19326  filuni  19417  rnelfmlem  19484  fmufil  19491  fclscf  19557  fclsfnflim  19559  flimfnfcls  19560  uffclsflim  19563  cnpfcfi  19572  cnpfcf  19573  alexsublem  19575  alexsubALTlem3  19580  tgpconcompeqg  19641  ghmcnp  19644  divstgplem  19650  blssps  19958  blss  19959  blcld  20039  metequiv2  20044  met2ndci  20056  prdsxmslem2  20063  txmetcnp  20081  nlmvscnlem1  20226  xrge0tsms  20370  ipcnlem1  20716  iscmet3  20763  cmetss  20784  minveclem3  20875  pmltpc  20893  ovolscalem2  20956  ovolicc2lem5  20963  ovolicc2  20964  nulmbl2  20977  ioombl1  21002  uniioombllem6  21027  uniioombl  21028  vitalilem3  21049  i1faddlem  21130  mbfmullem  21162  itg2const2  21178  itg2split  21186  lhop2  21446  dvfsumrlim  21462  itgsubst  21480  plydivex  21722  plyexmo  21738  ulmbdd  21822  cxploglim  22330  dchrptlem2  22563  lgsquad2lem2  22657  2sqlem5  22666  dchrvmasumif  22711  rpvmasum2  22720  dchrisum0re  22721  dchrisum0lem3  22727  dchrisum0  22728  dchrmusum  22732  dchrvmasum  22733  pntibndlem3  22800  pntlemp  22818  ostth3  22846  legtrid  22977  mirreu3  23010  ax5seglem9  23118  ax5seg  23119  axcontlem8  23152  axcontlem12  23156  ablo4  23709  smcnlem  24027  pjhthmo  24640  xrge0tsmsd  26188  xpinpreima2  26273  qqhval2  26347  dya2iocnrect  26632  orvcgteel  26780  orvclteel  26785  cnpcon  27049  txpcon  27051  conpcon  27054  pconpi1  27056  iccllyscon  27069  rellyscon  27070  cvmcov2  27094  cvmliftmolem2  27101  cvmliftmo  27103  cvmliftlem15  27117  cvmliftpht  27137  cvmlift3lem2  27139  relexpsucl  27263  relexpcnv  27264  relexpdm  27266  relexprn  27267  relexpadd  27269  relexpindlem  27270  rtrclreclem.min  27278  rtrclind  27280  prodmo  27378  fprod2dlem  27420  cgrextend  27968  btwnouttr2  27982  btwnexch2  27983  cgrxfr  28015  lineext  28036  btwnconn1lem5  28051  btwnconn1lem13  28059  btwnconn3  28063  segletr  28074  segleantisym  28075  outsideofeq  28090  outsidele  28092  lineunray  28107  mblfinlem3  28355  mblfinlem4  28356  cnambfre  28365  itg2addnclem  28368  areacirclem5  28413  comppfsc  28504  neibastop2lem  28506  neibastop2  28507  istotbnd3  28595  crngm4  28728  mzpmfp  29008  mzpmfpOLD  29009  mzpcompact2lem  29013  diophin  29036  pellexlem3  29097  pellex  29101  pell14qrmulcl  29129  jm2.19lem3  29265  jm2.25  29273  jm2.27b  29280  fnwe2lem2  29329  hbtlem2  29405  hbtlem5  29409  fnchoice  29676  stoweidlem53  29773  stoweidlem61  29781  wlkiswwlkfun  30274  wwlkextwrd  30285  usg2spthonot0  30333  frgranbnb  30537  frgrancvvdeqlemC  30557  scmatsubcl  30767  scmatmulcl  30769  cvlcvr1  32706  4atlem12  32978  cdlemb  33160  paddasslem10  33195  paddasslem12  33197  paddasslem13  33198  lhpexle3lem  33377  cdlemd4  33567  cdlemefs32sn1aw  33780  cdleme43fsv1snlem  33786  cdleme32d  33810  cdleme32f  33812  cdleme40m  33833  cdleme40n  33834  cdleme50trn2  33917  cdlemftr3  33931  cdlemm10N  34485  dihvalcqpre  34602  dihopelvalcpre  34615  dihmeetlem1N  34657  dihglblem5apreN  34658  dihmeetlem4preN  34673  dihjat1lem  34795  mapd0  35032  mapdh9a  35157