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  6020  grpridd  6318  mapdom2  7497  domunfican  7599  fofinf1o  7607  finsschain  7633  wemaplem3  7777  oemapvali  7907  iunfictbso  8299  enfin2i  8505  fin1a2s  8598  distrlem4pr  9210  divdivdiv  10047  divsubdiv  10062  lediv12a  10240  xralrple  11190  seqcaopr  11858  leexp2r  11936  hashbclem  12220  wrd2ind  12387  cshwidxmod  12455  rlimresb  13058  summo  13209  fsum2dlem  13252  bezoutlem3  13739  bezoutlem4  13740  qredeu  13808  pcqmul  13935  pcadd  13966  pockthg  13982  ramub1lem2  14103  cshwsdisj  14140  mreexexlem4d  14600  issubc3  14774  cofucl  14813  setcmon  14970  setcepi  14971  drsdirfi  15123  poslubmo  15331  posglbmo  15332  ghmpreima  15783  gaorber  15841  psgnunilem4  16018  psgneu  16027  odcau  16118  pgpssslw  16128  fislw  16139  lsmsubm  16167  efgsfo  16251  pgpfac1  16596  pgpfaclem2  16598  pgpfaclem3  16599  unitgrp  16774  islmodd  16969  lmodprop2d  17022  lsspropd  17113  lbsextlem4  17257  assapropd  17413  evlslem1  17616  mdetunilem8  18440  mdetmul  18444  ppttop  18626  epttop  18628  restbas  18777  iscnp4  18882  cnpco  18886  nrmsep  18976  regsep2  18995  ordthauslem  19002  1stcfb  19064  2ndcctbss  19074  2ndcdisj  19075  2ndcomap  19077  dis2ndc  19079  1stcelcls  19080  nlly2i  19095  islly2  19103  hausllycmp  19113  lly1stc  19115  1stckgenlem  19141  ptbasin  19165  txcls  19192  ptcnp  19210  txlly  19224  txnlly  19225  txtube  19228  txcmplem1  19229  txcmplem2  19230  xkococnlem  19247  basqtop  19299  regr1lem  19327  kqreglem1  19329  kqreglem2  19330  kqnrmlem1  19331  kqnrmlem2  19332  reghmph  19381  nrmhmph  19382  filuni  19473  rnelfmlem  19540  fmufil  19547  fclscf  19613  fclsfnflim  19615  flimfnfcls  19616  uffclsflim  19619  cnpfcfi  19628  cnpfcf  19629  alexsublem  19631  alexsubALTlem3  19636  tgpconcompeqg  19697  ghmcnp  19700  divstgplem  19706  blssps  20014  blss  20015  blcld  20095  metequiv2  20100  met2ndci  20112  prdsxmslem2  20119  txmetcnp  20137  nlmvscnlem1  20282  xrge0tsms  20426  ipcnlem1  20772  iscmet3  20819  cmetss  20840  minveclem3  20931  pmltpc  20949  ovolscalem2  21012  ovolicc2lem5  21019  ovolicc2  21020  nulmbl2  21033  ioombl1  21058  uniioombllem6  21083  uniioombl  21084  vitalilem3  21105  i1faddlem  21186  mbfmullem  21218  itg2const2  21234  itg2split  21242  lhop2  21502  dvfsumrlim  21518  itgsubst  21536  plydivex  21778  plyexmo  21794  ulmbdd  21878  cxploglim  22386  dchrptlem2  22619  lgsquad2lem2  22713  2sqlem5  22722  dchrvmasumif  22767  rpvmasum2  22776  dchrisum0re  22777  dchrisum0lem3  22783  dchrisum0  22784  dchrmusum  22788  dchrvmasum  22789  pntibndlem3  22856  pntlemp  22874  ostth3  22902  legtrid  23037  mirreu3  23073  ax5seglem9  23198  ax5seg  23199  axcontlem8  23232  axcontlem12  23236  ablo4  23789  smcnlem  24107  pjhthmo  24720  xrge0tsmsd  26268  xpinpreima2  26352  qqhval2  26426  dya2iocnrect  26711  orvcgteel  26865  orvclteel  26870  cnpcon  27134  txpcon  27136  conpcon  27139  pconpi1  27141  iccllyscon  27154  rellyscon  27155  cvmcov2  27179  cvmliftmolem2  27186  cvmliftmo  27188  cvmliftlem15  27202  cvmliftpht  27222  cvmlift3lem2  27224  relexpsucl  27349  relexpcnv  27350  relexpdm  27352  relexprn  27353  relexpadd  27355  relexpindlem  27356  rtrclreclem.min  27364  rtrclind  27366  prodmo  27464  fprod2dlem  27506  cgrextend  28054  btwnouttr2  28068  btwnexch2  28069  cgrxfr  28101  lineext  28122  btwnconn1lem5  28137  btwnconn1lem13  28145  btwnconn3  28149  segletr  28160  segleantisym  28161  outsideofeq  28176  outsidele  28178  lineunray  28193  mblfinlem3  28449  mblfinlem4  28450  cnambfre  28459  itg2addnclem  28462  areacirclem5  28507  comppfsc  28598  neibastop2lem  28600  neibastop2  28601  istotbnd3  28689  crngm4  28822  mzpmfp  29102  mzpmfpOLD  29103  mzpcompact2lem  29107  diophin  29130  pellexlem3  29191  pellex  29195  pell14qrmulcl  29223  jm2.19lem3  29359  jm2.25  29367  jm2.27b  29374  fnwe2lem2  29423  hbtlem2  29499  hbtlem5  29503  fnchoice  29770  stoweidlem53  29867  stoweidlem61  29875  wlkiswwlkfun  30368  wwlkextwrd  30379  usg2spthonot0  30427  frgranbnb  30631  frgrancvvdeqlemC  30651  scmatsubcl  30903  scmatmulcl  30905  cvlcvr1  33003  4atlem12  33275  cdlemb  33457  paddasslem10  33492  paddasslem12  33494  paddasslem13  33495  lhpexle3lem  33674  cdlemd4  33864  cdlemefs32sn1aw  34077  cdleme43fsv1snlem  34083  cdleme32d  34107  cdleme32f  34109  cdleme40m  34130  cdleme40n  34131  cdleme50trn2  34214  cdlemftr3  34228  cdlemm10N  34782  dihvalcqpre  34899  dihopelvalcpre  34912  dihmeetlem1N  34954  dihglblem5apreN  34955  dihmeetlem4preN  34970  dihjat1lem  35092  mapd0  35329  mapdh9a  35454