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

Theorem simprrr 742
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 448 . 2  |-  ( ( ch  /\  th )  ->  th )
21ad2antll 710 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  fliftfun  5997  grpridd  6250  mapdom2  7241  domunfican  7342  fofinf1o  7350  finsschain  7375  wemaplem3  7477  oemapvali  7600  iunfictbso  7955  enfin2i  8161  fin1a2s  8254  distrlem4pr  8863  divdivdiv  9675  divsubdiv  9690  lediv12a  9863  xralrple  10751  seqcaopr  11319  leexp2r  11396  hashbclem  11660  rlimresb  12318  summo  12470  fsum2dlem  12513  bezoutlem3  12999  bezoutlem4  13000  qredeu  13066  pcqmul  13186  pcadd  13217  pockthg  13233  ramub1lem2  13354  mreexexlem4d  13831  issubc3  14005  cofucl  14044  setcmon  14201  setcepi  14202  drsdirfi  14354  poslubmo  14532  ghmpreima  14986  gaorber  15044  odcau  15197  pgpssslw  15207  fislw  15218  lsmsubm  15246  efgsfo  15330  pgpfac1  15597  pgpfaclem2  15599  pgpfaclem3  15600  unitgrp  15731  islmodd  15915  lmodprop2d  15965  lsspropd  16052  lbsextlem4  16192  assapropd  16345  ppttop  17030  epttop  17032  restbas  17180  iscnp4  17285  cnpco  17289  nrmsep  17379  regsep2  17398  ordthauslem  17405  1stcfb  17465  2ndcctbss  17475  2ndcdisj  17476  2ndcomap  17478  dis2ndc  17480  1stcelcls  17481  nlly2i  17496  islly2  17504  hausllycmp  17514  lly1stc  17516  1stckgenlem  17542  ptbasin  17566  txcls  17593  ptcnp  17611  txlly  17625  txnlly  17626  txtube  17629  txcmplem1  17630  txcmplem2  17631  xkococnlem  17648  basqtop  17700  regr1lem  17728  kqreglem1  17730  kqreglem2  17731  kqnrmlem1  17732  kqnrmlem2  17733  reghmph  17782  nrmhmph  17783  filuni  17874  rnelfmlem  17941  fmufil  17948  fclscf  18014  fclsfnflim  18016  flimfnfcls  18017  uffclsflim  18020  cnpfcfi  18029  cnpfcf  18030  alexsublem  18032  alexsubALTlem3  18037  tgpconcompeqg  18098  ghmcnp  18101  divstgplem  18107  blssps  18411  blss  18412  blcld  18492  metequiv2  18497  met2ndci  18509  prdsxmslem2  18516  txmetcnp  18534  nlmvscnlem1  18679  xrge0tsms  18822  ipcnlem1  19156  iscmet3  19203  cmetss  19224  minveclem3  19287  pmltpc  19304  ovolscalem2  19367  ovolicc2lem5  19374  ovolicc2  19375  nulmbl2  19388  ioombl1  19413  uniioombllem6  19437  uniioombl  19438  vitalilem3  19459  i1faddlem  19542  mbfmullem  19574  itg2const2  19590  itg2split  19598  lhop2  19856  dvfsumrlim  19872  itgsubst  19890  evlslem1  19893  plydivex  20171  plyexmo  20187  ulmbdd  20271  cxploglim  20773  dchrptlem2  21006  lgsquad2lem2  21100  2sqlem5  21109  dchrvmasumif  21154  rpvmasum2  21163  dchrisum0re  21164  dchrisum0lem3  21170  dchrisum0  21171  dchrmusum  21175  dchrvmasum  21176  pntibndlem3  21243  pntlemp  21261  ostth3  21289  ablo4  21832  smcnlem  22150  pjhthmo  22761  xrge0tsmsd  24180  xpinpreima2  24262  qqhval2  24323  dya2iocnrect  24588  orvcgteel  24682  orvclteel  24687  cnpcon  24874  txpcon  24876  conpcon  24879  pconpi1  24881  iccllyscon  24894  rellyscon  24895  cvmcov2  24919  cvmliftmolem2  24926  cvmliftmo  24928  cvmliftlem15  24942  cvmliftpht  24962  cvmlift3lem2  24964  relexpsucl  25089  relexpcnv  25090  relexpdm  25092  relexprn  25093  relexpadd  25095  relexpindlem  25096  rtrclreclem.min  25104  rtrclind  25106  prodmo  25219  fprod2dlem  25261  ax5seglem9  25784  ax5seg  25785  axcontlem8  25818  axcontlem12  25822  cgrextend  25850  btwnouttr2  25864  btwnexch2  25865  cgrxfr  25897  lineext  25918  btwnconn1lem5  25933  btwnconn1lem13  25941  btwnconn3  25945  segletr  25956  segleantisym  25957  outsideofeq  25972  outsidele  25974  lineunray  25989  mblfinlem2  26148  mblfinlem3  26149  cnambfre  26158  itg2addnclem  26159  areacirclem6  26190  comppfsc  26281  neibastop2lem  26283  neibastop2  26284  istotbnd3  26374  crngm4  26507  mzpmfp  26698  mzpcompact2lem  26702  diophin  26725  pellexlem3  26788  pellex  26792  pell14qrmulcl  26820  jm2.19lem3  26956  jm2.25  26964  jm2.27b  26971  fnwe2lem2  27020  hbtlem2  27200  hbtlem5  27204  psgnunilem4  27292  psgneu  27301  fnchoice  27571  stoweidlem53  27673  stoweidlem61  27681  usg2spthonot0  28090  frgranbnb  28128  frgrancvvdeqlemC  28146  cvlcvr1  29826  4atlem12  30098  cdlemb  30280  paddasslem10  30315  paddasslem12  30317  paddasslem13  30318  lhpexle3lem  30497  cdlemd4  30687  cdlemefs32sn1aw  30900  cdleme43fsv1snlem  30906  cdleme32d  30930  cdleme32f  30932  cdleme40m  30953  cdleme40n  30954  cdleme50trn2  31037  cdlemftr3  31051  cdlemm10N  31605  dihvalcqpre  31722  dihopelvalcpre  31735  dihmeetlem1N  31777  dihglblem5apreN  31778  dihmeetlem4preN  31793  dihjat1lem  31915  mapd0  32152  mapdh9a  32277
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 178  df-an 361
  Copyright terms: Public domain W3C validator