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

Theorem simpr3 1005
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )

Proof of Theorem simpr3
StepHypRef Expression
1 simp3 999 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 466 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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  df-3an 976
This theorem is referenced by:  simplr3  1041  simprr3  1047  simp1r3  1095  simp2r3  1101  simp3r3  1107  3anandis  1331  isopolem  6226  fr3nr  6600  suppfnss  6927  elfir  7877  intrnfi  7878  fisupcl  7930  cnfcomlem  8146  cnfcomlemOLD  8154  ackbij1lem15  8617  pwfseqlem4a  9042  pwfseqlem4  9043  eluzuzle  11100  xlesubadd  11466  elioc2  11598  elico2  11599  elicc2  11600  fseq1p1m1  11763  swrdsymbeq  12654  ccatswrd  12663  modfsummods  13589  tanadd  13884  dvds2ln  13996  cshwsidrepsw  14560  ressress  14676  f1ovscpbl  14905  mreexexlem4d  15026  mreexexd  15027  2oppccomf  15102  fthmon  15275  fuccocl  15312  fucidcl  15313  invfuc  15322  curf2cl  15479  yonedalem4c  15525  yonedalem3  15528  pospo  15582  latjle12  15671  latjlej1  15674  latnlej2  15680  latlem12  15687  latmlem1  15690  latledi  15698  latjass  15704  latj12  15705  latj32  15706  latj13  15707  latj31  15708  latjrot  15709  latjjdi  15712  latjjdir  15713  latdisdlem  15798  prdsmndd  15932  imasmnd2  15936  imasmnd  15937  frmdmnd  16006  grpsubadd  16105  grpaddsubass  16107  grpsubsub4  16110  grppnpcan2  16111  grpnpncan  16112  grpnnncan2  16114  mulgnndir  16143  mulgnn0dir  16144  mulgnnass  16149  mulgnn0ass  16150  mulgass  16151  pwsmulg  16163  imasgrp2  16164  imasgrp  16165  issubg2  16195  qusgrp  16235  galcan  16321  gacan  16322  oppgmnd  16368  symggrp  16404  pmtrprfv  16457  pmtr3ncom  16479  psgnunilem3  16500  frgp0  16757  cmn32  16795  cmn12  16797  abladdsub  16804  mulgdi  16814  mulgsubdi  16817  dprdss  17055  dprdf1o  17058  dprdsn  17062  dmdprdsplit  17075  pgpfac1lem5  17109  srgi  17142  ringi  17190  prdsringd  17240  imasring  17247  opprring  17259  mulgass3  17265  dvrass  17318  kerf1hrm  17371  subrgunit  17426  issubrg2  17428  abvdiv  17465  lss1  17564  lsssn0  17573  islss3  17584  prdslmodd  17594  islmhm2  17663  lspsolv  17768  lbsextlem4  17786  sralmod  17812  issubassa  17952  sraassa  17953  psrbaglesupp  17996  psrbaglesuppOLD  17997  psrbagcon  18001  psrgrp  18030  psrlmod  18033  psrring  18045  psrassa  18048  mpllsslem  18073  mpllsslemOLD  18075  ipdi  18653  ipsubdir  18655  ipsubdi  18656  ipassr  18659  ipassr2  18660  isphld  18667  ocvlss  18681  mamudm  18868  matring  18923  matassa  18924  ofco2  18931  scmatlss  19005  ma1repveval  19051  mdetunilem1  19092  mdetunilem9  19100  monmatcollpw  19258  iinopn  19389  restopnb  19654  subbascn  19733  nrmsep2  19835  isnrm3  19838  t1sep  19849  regsep2  19855  dnsconst  19857  dfcon2  19898  dislly  19976  tx1stc  20129  qtophmeo  20296  filss  20332  infil  20342  fsubbas  20346  filssufilg  20390  hauspwpwf1  20466  cnextcn  20545  tmdcn2  20566  psmettri  20793  isxmet2d  20808  xmettri  20832  xmetres2  20842  bldisj  20879  blss2ps  20884  blss2  20885  xmstri2  20947  mstri2  20948  xmstri  20949  mstri  20950  xmstri3  20951  mstri3  20952  msrtri  20953  comet  20994  met2ndci  21003  ngprcan  21107  ngplcan  21108  ngpsubcan  21111  nrgdsdi  21152  nrgdsdir  21153  nlmdsdi  21168  nlmdsdir  21169  blcvx  21281  iocopnst  21418  icccvx  21428  pi1grplem  21527  pi1xfrf  21531  pi1cof  21537  cvsdiv  21587  cvsdivcl  21588  cphdivcl  21607  cphsubdir  21632  cphsubdi  21633  bcthlem5  21745  rrxcph  21802  volfiniun  21935  volcn  21993  itg1val2  22069  dvconst  22298  dvlip  22372  ftc1a  22416  ulmdvlem3  22775  ang180  23124  cvxcl  23292  scvxcvx  23293  sgmmul  23454  logexprlim  23478  dchrabl  23507  motgrp  23908  f1otrge  24153  xmstrkgc  24167  colinearalglem1  24187  colinearalg  24191  axcgrtr  24196  axlowdimlem16  24238  axeuclidlem  24243  axcontlem4  24248  axcontlem7  24251  axcontlem12  24256  eengtrkg  24266  eengtrkge  24267  isspthonpth  24564  wlkdvspth  24588  usg2wotspth  24862  2pthwlkonot  24863  rusgranumwwlkg  24937  numclwwlk5  25090  friendship  25100  grpomuldivass  25229  grpopnpcan2  25233  grponpncan  25235  grpodiveq  25236  ablodivdiv4  25271  ablonnncan  25273  ismndo1  25324  nvsubadd  25528  dipdi  25736  dipsubdi  25742  disjdsct  27499  omndmul2  27680  archiabllem2c  27717  dvrdir  27758  dvrcan5  27761  reofld  27808  pstmfval  27853  qqhval2lem  27940  qqhvq  27946  esumcvg  28070  sigaclcu  28095  measdivcstOLD  28173  measdivcst  28174  erdszelem9  28621  cvmseu  28699  elmrsubrn  28858  cgrid2  29629  btwncomim  29639  btwnswapid  29643  trisegint  29654  cgrxfr  29681  btwnxfr  29682  brofs2  29703  brifs2  29704  endofsegid  29711  btwnconn1lem11  29723  btwnconn2  29728  segcon2  29731  seglemin  29739  segletr  29740  btwnsegle  29743  colinbtwnle  29744  broutsideof2  29748  btwnoutside  29751  broutsideof3  29752  outsideoftr  29755  outsidele  29758  ellines  29778  linethrueu  29782  ftc1anc  30074  sdclem1  30212  sstotbnd2  30246  zerdivemp1x  30334  isdrngo2  30337  iscringd  30372  irrapxlem6  30739  jm2.26lem3  30919  mpaamn  31081  mendring  31117  mendlmod  31118  mendassa  31119  rfcnpre4  31363  fmuldfeq  31531  stoweidlem43  31779  stoweidlem52  31788  stoweidlem53  31789  stoweidlem56  31792  copissgrp  32449  ringrng  32523  cznrng  32590  funcringcsetcOLD2lem9  32724  funcringcsetclem9OLD  32747  linccl  32885  lincsumscmcl  32904  ldepsprlem  32943  lincresunit3lem1  32950  bnj970  33873  bnj910  33874  lsmsat  34608  lfladdcl  34671  lflnegcl  34675  lflvscl  34677  lshpkrlem4  34713  lshpkrlem6  34715  ldualgrplem  34745  lduallmodlem  34752  latmassOLD  34829  latm12  34830  latm32  34831  latmrot  34832  latmmdiN  34834  latmmdir  34835  omlfh1N  34858  omlfh3N  34859  cvrnbtwn2  34875  cvlexchb1  34930  cvlexch3  34932  cvlexch4N  34933  cvlatexchb1  34934  cvlsupr2  34943  hlatjass  34969  hlatj12  34970  hlatj32  34971  cvrat  35021  atcvrj0  35027  cvrat2  35028  atltcvr  35034  atexchltN  35040  cvrat3  35041  cvrat4  35042  atbtwnexOLDN  35046  atbtwnex  35047  3dimlem3  35060  3dimlem3OLDN  35061  3at  35089  2atneat  35114  llncmp  35121  2at0mat0  35124  2atmat0  35125  islpln2a  35147  llncvrlpln  35157  lplncmp  35161  3atnelvolN  35185  4atlem11  35208  lplncvrlvol  35215  lvolcmp  35216  2atm2atN  35384  elpaddatriN  35402  elpadd2at2  35406  paddasslem8  35426  paddasslem17  35435  paddass  35437  padd12N  35438  paddssw1  35442  pmodlem2  35446  pmodN  35449  pmapjlln1  35454  atmod1i2  35458  pexmidlem2N  35570  pexmidlem7N  35575  pl42lem2N  35579  pl42lem3N  35580  pl42lem4N  35581  pl42N  35582  lhp2lt  35600  lhpm0atN  35628  lautlt  35690  lautcvr  35691  lautj  35692  lautm  35693  ltrneq2  35747  cdleme1b  35826  cdleme3b  35829  cdleme3c  35830  cdleme9b  35852  cdlemefs27cl  36014  cdleme42mN  36088  cdlemg4c  36213  trljco  36341  tgrpgrplem  36350  tendoplass  36384  tendodi1  36385  tendodi2  36386  erngplus2  36405  erngplus2-rN  36413  cdlemk36  36514  erngdvlem3  36591  erngdvlem3-rN  36599  dvaplusgv  36611  tendospass  36621  tendospdi1  36622  dvalveclem  36627  dialss  36648  dvhvaddass  36699  dvhopvsca  36704  dvhlveclem  36710  diblss  36772  diclss  36795  diclspsn  36796  cdlemn11pre  36812  dihmeetlem12N  36920  dihmeetlem16N  36924  dihmeetlem17N  36925  dvh4dimN  37049  lpolsatN  37090  lpolpolsatN  37091  dochpolN  37092  lclkr  37135  lclkrs  37141  lcfr  37187
  Copyright terms: Public domain W3C validator