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

Theorem simpr3 1004
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 998 . 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 973
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 975
This theorem is referenced by:  simplr3  1040  simprr3  1046  simp1r3  1094  simp2r3  1100  simp3r3  1106  3anandis  1330  isopolem  6228  fr3nr  6594  suppfnss  6925  elfir  7874  intrnfi  7875  fisupcl  7926  cnfcomlem  8142  cnfcomlemOLD  8150  ackbij1lem15  8613  pwfseqlem4a  9038  pwfseqlem4  9039  eluzuzle  11089  xlesubadd  11454  elioc2  11586  elico2  11587  elicc2  11588  fseq1p1m1  11751  swrdsymbeq  12634  ccatswrd  12643  modfsummods  13569  tanadd  13762  dvds2ln  13874  cshwsidrepsw  14435  ressress  14551  f1ovscpbl  14780  mreexexlem4d  14901  mreexexd  14902  2oppccomf  14980  fthmon  15153  fuccocl  15190  fucidcl  15191  invfuc  15200  curf2cl  15357  yonedalem4c  15403  yonedalem3  15406  pospo  15459  latjle12  15548  latjlej1  15551  latnlej2  15557  latlem12  15564  latmlem1  15567  latledi  15575  latjass  15581  latj12  15582  latj32  15583  latj13  15584  latj31  15585  latjrot  15586  latjjdi  15589  latjjdir  15590  latdisdlem  15675  prdsmndd  15771  imasmnd2  15775  imasmnd  15776  frmdmnd  15856  grpsubadd  15933  grpaddsubass  15935  grpsubsub4  15938  grppnpcan2  15939  grpnpncan  15940  grpnnncan2  15942  mulgnndir  15971  mulgnn0dir  15972  mulgnnass  15977  mulgnn0ass  15978  mulgass  15979  pwsmulg  15991  imasgrp2  15992  imasgrp  15993  issubg2  16018  divsgrp  16058  galcan  16144  gacan  16145  oppgmnd  16191  symggrp  16227  pmtrprfv  16281  pmtr3ncom  16303  psgnunilem3  16324  frgp0  16581  cmn32  16619  cmn12  16621  abladdsub  16628  mulgdi  16638  mulgsubdi  16641  dprdss  16875  dprdf1o  16878  dprdsn  16882  dmdprdsplit  16895  pgpfac1lem5  16929  srgi  16962  rngi  17007  prdsrngd  17057  imasrng  17064  opprrng  17076  mulgass3  17082  dvrass  17135  kerf1hrm  17187  subrgunit  17242  issubrg2  17244  abvdiv  17281  lss1  17380  lsssn0  17389  islss3  17400  prdslmodd  17410  islmhm2  17479  lspsolv  17584  lbsextlem4  17602  sralmod  17628  issubassa  17760  sraassa  17761  psrbaglesupp  17804  psrbaglesuppOLD  17805  psrbagcon  17809  psrgrp  17838  psrlmod  17841  psrrng  17853  psrassa  17856  mpllsslem  17881  mpllsslemOLD  17883  ipdi  18458  ipsubdir  18460  ipsubdi  18461  ipassr  18464  ipassr2  18465  isphld  18472  ocvlss  18486  mamudm  18673  matrng  18728  matassa  18729  ofco2  18736  scmatlss  18810  ma1repveval  18856  mdetunilem1  18897  mdetunilem9  18905  monmatcollpw  19063  iinopn  19194  restopnb  19458  subbascn  19537  nrmsep2  19639  isnrm3  19642  t1sep  19653  regsep2  19659  dnsconst  19661  dfcon2  19702  dislly  19780  tx1stc  19902  qtophmeo  20069  filss  20105  infil  20115  fsubbas  20119  filssufilg  20163  hauspwpwf1  20239  cnextcn  20318  tmdcn2  20339  psmettri  20566  isxmet2d  20581  xmettri  20605  xmetres2  20615  bldisj  20652  blss2ps  20657  blss2  20658  xmstri2  20720  mstri2  20721  xmstri  20722  mstri  20723  xmstri3  20724  mstri3  20725  msrtri  20726  comet  20767  met2ndci  20776  ngprcan  20880  ngplcan  20881  ngpsubcan  20884  nrgdsdi  20925  nrgdsdir  20926  nlmdsdi  20941  nlmdsdir  20942  blcvx  21054  iocopnst  21191  icccvx  21201  pi1grplem  21300  pi1xfrf  21304  pi1cof  21310  cvsdiv  21360  cvsdivcl  21361  cphdivcl  21380  cphsubdir  21405  cphsubdi  21406  bcthlem5  21518  rrxcph  21575  volfiniun  21708  volcn  21766  itg1val2  21842  dvconst  22071  dvlip  22145  ftc1a  22189  ulmdvlem3  22547  ang180  22890  cvxcl  23058  scvxcvx  23059  sgmmul  23220  logexprlim  23244  dchrabl  23273  motgrp  23674  f1otrge  23867  xmstrkgc  23881  colinearalglem1  23901  colinearalg  23905  axcgrtr  23910  axlowdimlem16  23952  axeuclidlem  23957  axcontlem4  23962  axcontlem7  23965  axcontlem12  23970  eengtrkg  23980  eengtrkge  23981  isspthonpth  24278  wlkdvspth  24302  usg2wotspth  24576  2pthwlkonot  24577  rusgranumwwlkg  24651  numclwwlk5  24805  friendship  24815  grpomuldivass  24943  grpopnpcan2  24947  grponpncan  24949  grpodiveq  24950  ablodivdiv4  24985  ablonnncan  24987  ismndo1  25038  nvsubadd  25242  dipdi  25450  dipsubdi  25456  disjdsct  27209  omndmul2  27380  archiabllem2c  27417  dvrdir  27459  dvrcan5  27462  reofld  27509  pstmfval  27527  qqhval2lem  27614  qqhvq  27620  esumcvg  27748  sigaclcu  27773  measdivcstOLD  27851  measdivcst  27852  erdszelem9  28299  cvmseu  28377  cgrid2  29246  btwncomim  29256  btwnswapid  29260  trisegint  29271  cgrxfr  29298  btwnxfr  29299  brofs2  29320  brifs2  29321  endofsegid  29328  btwnconn1lem11  29340  btwnconn2  29345  segcon2  29348  seglemin  29356  segletr  29357  btwnsegle  29360  colinbtwnle  29361  broutsideof2  29365  btwnoutside  29368  broutsideof3  29369  outsideoftr  29372  outsidele  29375  ellines  29395  linethrueu  29399  ftc1anc  29691  sdclem1  29855  sstotbnd2  29889  zerdivemp1x  29977  isdrngo2  29980  iscringd  30015  irrapxlem6  30383  jm2.26lem3  30563  mpaamn  30726  mendrng  30762  mendlmod  30763  mendassa  30764  rfcnpre4  31003  fmuldfeq  31149  stoweidlem43  31359  stoweidlem52  31368  stoweidlem53  31369  stoweidlem56  31372  ringrng0  32002  linccl  32105  lincsumscmcl  32124  lincresunit3lem1  32170  bnj970  33093  bnj910  33094  lsmsat  33814  lfladdcl  33877  lflnegcl  33881  lflvscl  33883  lshpkrlem4  33919  lshpkrlem6  33921  ldualgrplem  33951  lduallmodlem  33958  latmassOLD  34035  latm12  34036  latm32  34037  latmrot  34038  latmmdiN  34040  latmmdir  34041  omlfh1N  34064  omlfh3N  34065  cvrnbtwn2  34081  cvlexchb1  34136  cvlexch3  34138  cvlexch4N  34139  cvlatexchb1  34140  cvlsupr2  34149  hlatjass  34175  hlatj12  34176  hlatj32  34177  cvrat  34227  atcvrj0  34233  cvrat2  34234  atltcvr  34240  atexchltN  34246  cvrat3  34247  cvrat4  34248  atbtwnexOLDN  34252  atbtwnex  34253  3dimlem3  34266  3dimlem3OLDN  34267  3at  34295  2atneat  34320  llncmp  34327  2at0mat0  34330  2atmat0  34331  islpln2a  34353  llncvrlpln  34363  lplncmp  34367  3atnelvolN  34391  4atlem11  34414  lplncvrlvol  34421  lvolcmp  34422  2atm2atN  34590  elpaddatriN  34608  elpadd2at2  34612  paddasslem8  34632  paddasslem17  34641  paddass  34643  padd12N  34644  paddssw1  34648  pmodlem2  34652  pmodN  34655  pmapjlln1  34660  atmod1i2  34664  pexmidlem2N  34776  pexmidlem7N  34781  pl42lem2N  34785  pl42lem3N  34786  pl42lem4N  34787  pl42N  34788  lhp2lt  34806  lhpm0atN  34834  lautlt  34896  lautcvr  34897  lautj  34898  lautm  34899  ltrneq2  34953  cdleme1b  35031  cdleme3b  35034  cdleme3c  35035  cdleme9b  35057  cdlemefs27cl  35218  cdleme42mN  35292  cdlemg4c  35417  trljco  35545  tgrpgrplem  35554  tendoplass  35588  tendodi1  35589  tendodi2  35590  erngplus2  35609  erngplus2-rN  35617  cdlemk36  35718  erngdvlem3  35795  erngdvlem3-rN  35803  dvaplusgv  35815  tendospass  35825  tendospdi1  35826  dvalveclem  35831  dialss  35852  dvhvaddass  35903  dvhopvsca  35908  dvhlveclem  35914  diblss  35976  diclss  35999  diclspsn  36000  cdlemn11pre  36016  dihmeetlem12N  36124  dihmeetlem16N  36128  dihmeetlem17N  36129  dvh4dimN  36253  lpolsatN  36294  lpolpolsatN  36295  dochpolN  36296  lclkr  36339  lclkrs  36345  lcfr  36391
  Copyright terms: Public domain W3C validator