MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprrr Unicode version

Theorem simprrr 741
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
StepHypRef Expression
1 simpr 447 . 2  |-  ( ( ch  /\  th )  ->  th )
21ad2antll 709 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  fliftfun  5811  grpridd  6060  mapdom2  7032  domunfican  7129  fofinf1o  7137  finsschain  7162  wemaplem3  7263  oemapvali  7386  iunfictbso  7741  enfin2i  7947  fin1a2s  8040  distrlem4pr  8650  divdivdiv  9461  divsubdiv  9476  lediv12a  9649  xralrple  10532  seqcaopr  11083  leexp2r  11159  hashbclem  11390  rlimresb  12039  summo  12190  fsum2dlem  12233  bezoutlem3  12719  bezoutlem4  12720  qredeu  12786  pcqmul  12906  pcadd  12937  pockthg  12953  ramub1lem2  13074  mreexexlem4d  13549  issubc3  13723  cofucl  13762  setcmon  13919  setcepi  13920  drsdirfi  14072  poslubmo  14250  ghmpreima  14704  gaorber  14762  odcau  14915  pgpssslw  14925  fislw  14936  lsmsubm  14964  efgsfo  15048  pgpfac1  15315  pgpfaclem2  15317  pgpfaclem3  15318  unitgrp  15449  islmodd  15633  lmodprop2d  15687  lsspropd  15774  lbsextlem4  15914  assapropd  16067  ppttop  16744  epttop  16746  restbas  16889  cnpco  16996  nrmsep  17085  regsep2  17104  ordthauslem  17111  1stcfb  17171  2ndcctbss  17181  2ndcdisj  17182  2ndcomap  17184  dis2ndc  17186  1stcelcls  17187  nlly2i  17202  islly2  17210  hausllycmp  17220  lly1stc  17222  1stckgenlem  17248  ptbasin  17272  txcls  17299  ptcnp  17316  txlly  17330  txnlly  17331  txtube  17334  txcmplem1  17335  txcmplem2  17336  xkococnlem  17353  basqtop  17402  regr1lem  17430  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  reghmph  17484  nrmhmph  17485  filuni  17580  rnelfmlem  17647  fmufil  17654  fclscf  17720  fclsfnflim  17722  flimfnfcls  17723  uffclsflim  17726  cnpfcfi  17735  cnpfcf  17736  alexsublem  17738  alexsubALTlem3  17743  tgpconcompeqg  17794  ghmcnp  17797  divstgplem  17803  blss  17972  blcld  18051  metequiv2  18056  met2ndci  18068  prdsxmslem2  18075  txmetcnp  18093  nlmvscnlem1  18197  xrge0tsms  18339  ipcnlem1  18672  iscmet3  18719  cmetss  18740  minveclem3  18793  pmltpc  18810  ovolscalem2  18873  ovolicc2lem5  18880  ovolicc2  18881  nulmbl2  18894  ioombl1  18919  uniioombllem6  18943  uniioombl  18944  vitalilem3  18965  i1faddlem  19048  mbfmullem  19080  itg2const2  19096  itg2split  19104  lhop2  19362  dvfsumrlim  19378  itgsubst  19396  evlslem1  19399  plydivex  19677  plyexmo  19693  ulmbdd  19775  cxploglim  20272  dchrptlem2  20504  lgsquad2lem2  20598  2sqlem5  20607  dchrvmasumif  20652  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem3  20668  dchrisum0  20669  dchrmusum  20673  dchrvmasum  20674  pntibndlem3  20741  pntlemp  20759  ostth3  20787  ablo4  20954  smcnlem  21270  pjhthmo  21881  xpinpreima2  23291  xrge0tsmsd  23382  orvcgteel  23668  orvclteel  23673  cnpcon  23761  txpcon  23763  conpcon  23766  pconpi1  23768  iccllyscon  23781  rellyscon  23782  cvmcov2  23806  cvmliftmolem2  23813  cvmliftmo  23815  cvmliftlem15  23829  cvmliftpht  23849  cvmlift3lem2  23851  relexpsucl  24028  relexpcnv  24029  relexpdm  24032  relexprn  24033  relexpadd  24035  relexpindlem  24036  rtrclreclem.min  24044  rtrclind  24046  ax5seglem9  24565  ax5seg  24566  axcontlem8  24599  axcontlem12  24603  cgrextend  24631  btwnouttr2  24645  btwnexch2  24646  cgrxfr  24678  lineext  24699  btwnconn1lem5  24714  btwnconn1lem13  24722  btwnconn3  24726  segletr  24737  segleantisym  24738  outsideofeq  24753  outsidele  24755  lineunray  24770  areacirclem6  24930  fprodsub  25379  rltrooo  25415  iscnp4  25563  comppfsc  26307  neibastop2lem  26309  neibastop2  26310  istotbnd3  26495  crngm4  26628  mzpmfp  26825  mzpcompact2lem  26829  diophin  26852  pellexlem3  26916  pellex  26920  pell14qrmulcl  26948  jm2.19lem3  27084  jm2.25  27092  jm2.27b  27099  fnwe2lem2  27148  hbtlem2  27328  hbtlem5  27332  psgnunilem4  27420  psgneu  27429  fnchoice  27700  stoweidlem53  27802  cvlcvr1  29529  4atlem12  29801  cdlemb  29983  paddasslem10  30018  paddasslem12  30020  paddasslem13  30021  lhpexle3lem  30200  cdlemd4  30390  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme32d  30633  cdleme32f  30635  cdleme40m  30656  cdleme40n  30657  cdleme50trn2  30740  cdlemftr3  30754  cdlemm10N  31308  dihvalcqpre  31425  dihopelvalcpre  31438  dihmeetlem1N  31480  dihglblem5apreN  31481  dihmeetlem4preN  31496  dihjat1lem  31618  mapd0  31855  mapdh9a  31980
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator