Theorem simprrr 773

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  f1prex  6188  fliftfun  6211  grpridd  6514  wfrlem17  7051  mapdom2  7740  domunfican  7841  fofinf1o  7849  finsschain  7878  wemaplem3  8054  oemapvali  8179  iunfictbso  8534  enfin2i  8740  fin1a2s  8833  distrlem4pr  9440  mulcmpblnr  9484  prsrlem1  9485  addsrmo  9486  mulsrmo  9487  divdivdiv  10297  divsubdiv  10312  lediv12a  10488  xralrple  11487  seqcaopr  12236  leexp2r  12316  hashbclem  12599  wrd2ind  12808  cshwidxmod  12879  rtrclreclem4  13092  relexpindlem  13094  rtrclind  13096  rlimresb  13596  summo  13750  fsum2dlem  13798  prodmo  13957  fprod2dlem  14001  bezoutlem3  14468  bezoutlem4  14469  qredeu  14624  coprmproddvdslem  14639  pcqmul  14755  pcadd  14786  pockthg  14802  ramub1lem2  14937  cshwsdisj  15021  mreexexlem4d  15497  issubc3  15698  cofucl  15737  setcmon  15926  setcepi  15927  drsdirfi  16127  poslubmo  16336  posglbmo  16337  ghmpreima  16848  gaorber  16906  psgnunilem4  17082  psgneu  17091  odcau  17184  pgpssslw  17194  fislw  17205  lsmsubm  17233  efgsfo  17317  pgpfac1  17641  pgpfaclem2  17643  pgpfaclem3  17644  unitgrp  17823  islmodd  18025  lmodprop2d  18078  lsspropd  18168  lbsextlem4  18312  assapropd  18479  evlslem1  18666  mdetunilem8  19568  mdetmul  19572  ppttop  19946  epttop  19948  restbas  20098  iscnp4  20203  cnpco  20207  nrmsep  20297  regsep2  20316  ordthauslem  20323  1stcfb  20384  2ndcctbss  20394  2ndcdisj  20395  2ndcomap  20397  dis2ndc  20399  1stcelcls  20400  nlly2i  20415  islly2  20423  hausllycmp  20433  lly1stc  20435  comppfsc  20471  1stckgenlem  20492  ptbasin  20516  txcls  20543  ptcnp  20561  txlly  20575  txnlly  20576  txtube  20579  txcmplem1  20580  txcmplem2  20581  xkococnlem  20598  basqtop  20650  regr1lem  20678  kqreglem1  20680  kqreglem2  20681  kqnrmlem1  20682  kqnrmlem2  20683  reghmph  20732  nrmhmph  20733  filuni  20824  rnelfmlem  20891  fmufil  20898  fclscf  20964  fclsfnflim  20966  flimfnfcls  20967  uffclsflim  20970  cnpfcfi  20979  cnpfcf  20980  alexsublem  20983  alexsubALTlem3  20988  tgpconcompeqg  21050  ghmcnp  21053  qustgplem  21059  blssps  21363  blss  21364  blcld  21444  metequiv2  21449  met2ndci  21461  prdsxmslem2  21468  txmetcnp  21486  nlmvscnlem1  21613  xrge0tsms  21756  ipcnlem1  22102  iscmet3  22149  cmetss  22170  minveclem3  22257  pmltpc  22275  ovolscalem2  22341  ovolicc2lem5  22349  ovolicc2  22350  nulmbl2  22364  ioombl1  22389  uniioombllem6  22420  uniioombl  22421  vitalilem3  22442  i1faddlem  22525  mbfmullem  22557  itg2const2  22573  itg2split  22581  lhop2  22841  dvfsumrlim  22857  itgsubst  22875  plydivex  23115  plyexmo  23131  ulmbdd  23215  cxploglim  23765  dchrptlem2  24053  lgsquad2lem2  24147  2sqlem5  24156  dchrvmasumif  24201  rpvmasum2  24210  dchrisum0re  24211  dchrisum0lem3  24217  dchrisum0  24218  dchrmusum  24222  dchrvmasum  24223  pntibndlem3  24290  pntlemp  24308  ostth3  24336  legtrid  24493  hlcgreu  24519  mirreu3  24556  opphllem  24631  oppperpex  24649  lnperpex  24698  trgcopy  24699  iscgra1  24705  cgraswap  24715  cgracom  24717  cgratr  24718  acopyeu  24725  ax5seglem9  24810  ax5seg  24811  axcontlem8  24844  axcontlem12  24848  wlkiswwlkfun  25287  wwlkextwrd  25298  usg2spthonot0  25459  frgranbnb  25590  frgrancvvdeqlemC  25609  ablo4  25857  smcnlem  26175  pjhthmo  26787  1stpreimas  28123  xrge0tsmsd  28384  locfinref  28504  xpinpreima2  28549  qqhval2  28622  dya2iocnrect  28939  orvcgteel  29123  orvclteel  29128  cnpcon  29738  txpcon  29740  conpcon  29743  pconpi1  29745  iccllyscon  29758  rellyscon  29759  cvmcov2  29783  cvmliftmolem2  29790  cvmliftmo  29792  cvmliftlem15  29806  cvmliftpht  29826  cvmlift3lem2  29828  cgrextend  30557  btwnouttr2  30571  btwnexch2  30572  cgrxfr  30604  lineext  30625  btwnconn1lem5  30640  btwnconn1lem13  30648  btwnconn3  30652  segletr  30663  segleantisym  30664  outsideofeq  30679  outsidele  30681  lineunray  30696  refssfne  30796  neibastop2lem  30798  neibastop2  30799  mblfinlem3  31683  mblfinlem4  31684  cnambfre  31693  itg2addnclem  31697  areacirclem5  31740  istotbnd3  31807  crngm4  31940  cvlcvr1  32614  4atlem12  32886  cdlemb  33068  paddasslem10  33103  paddasslem12  33105  paddasslem13  33106  lhpexle3lem  33285  cdlemd4  33476  cdlemefs32sn1aw  33690  cdleme43fsv1snlem  33696  cdleme32d  33720  cdleme32f  33722  cdleme40m  33743  cdleme40n  33744  cdleme50trn2  33827  cdlemftr3  33841  cdlemm10N  34395  dihvalcqpre  34512  dihopelvalcpre  34525  dihmeetlem1N  34567  dihglblem5apreN  34568  dihmeetlem4preN  34583  dihjat1lem  34705  mapd0  34942  mapdh9a  35067  mzpmfp  35298  mzpcompact2lem  35302  diophin  35324  pellexlem3  35385  pellex  35389  pell14qrmulcl  35419  jm2.19lem3  35556  jm2.25  35564  jm2.27b  35571  fnwe2lem2  35619  hbtlem2  35693  hbtlem5  35697  gsumws3  36289  gsumws4  36290  fnchoice  36994  stoweidlem53  37487  stoweidlem61  37495  bgoldbtbnd  38307