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

Theorem simpr3 965
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 959 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 453 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simplr3  1001  simprr3  1007  simp1r3  1055  simp2r3  1061  simp3r3  1067  3anandis  1285  fr3nr  4719  isopolem  6024  elfir  7378  intrnfi  7379  fisupcl  7428  cnfcomlem  7612  ackbij1lem15  8070  pwfseqlem4a  8492  pwfseqlem4  8493  xlesubadd  10798  elioc2  10929  elico2  10930  elicc2  10931  fseq1p1m1  11077  ccatswrd  11728  tanadd  12723  dvds2ln  12835  ressress  13481  f1ovscpbl  13706  mreexexlem4d  13827  mreexexd  13828  2oppccomf  13906  fthmon  14079  fuccocl  14116  fucidcl  14117  invfuc  14126  curf2cl  14283  yonedalem4c  14329  yonedalem3  14332  pospo  14385  latjlej1  14449  latnlej2  14455  latmlem1  14465  latledi  14473  latjass  14479  latj12  14480  latj32  14481  latj13  14482  latj31  14483  latjrot  14484  latjjdi  14487  latjjdir  14488  latdisdlem  14570  prdsmndd  14683  imasmnd2  14687  imasmnd  14688  frmdmnd  14759  grpsubadd  14831  grpaddsubass  14833  grpsubsub4  14836  grppnpcan2  14837  grpnpncan  14838  grpnnncan2  14839  mulgnndir  14867  mulgnn0dir  14868  mulgnnass  14873  mulgnn0ass  14874  mulgass  14875  pwsmulg  14887  imasgrp2  14888  imasgrp  14889  issubg2  14914  divsgrp  14950  galcan  15036  gacan  15037  symggrp  15058  oppgmnd  15105  frgp0  15347  cmn32  15385  cmn12  15387  abladdsub  15394  mulgdi  15404  mulgsubdi  15407  dprdss  15542  dprdf1o  15545  dprdsn  15549  dmdprdsplit  15560  pgpfac1lem5  15592  rngi  15631  prdsrngd  15673  imasrng  15680  opprrng  15691  mulgass3  15697  dvrass  15750  subrgunit  15841  issubrg2  15843  abvdiv  15880  lss1  15970  lsssn0  15979  islss3  15990  prdslmodd  16000  islmhm2  16069  lspsolv  16170  lbsextlem4  16188  sralmod  16213  issubassa  16338  sraassa  16339  psrbaglesupp  16388  psrbagcon  16391  psrgrp  16417  psrlmod  16420  psrrng  16429  psrassa  16432  mpllsslem  16454  ipdi  16826  ipsubdir  16828  ipsubdi  16829  ipassr  16832  ipassr2  16833  isphld  16840  ocvlss  16854  iinopn  16930  restopnb  17193  subbascn  17272  nrmsep2  17374  isnrm3  17377  t1sep  17388  regsep2  17394  dnsconst  17396  dfcon2  17435  dislly  17513  tx1stc  17635  qtophmeo  17802  filss  17838  infil  17848  fsubbas  17852  filssufilg  17896  hauspwpwf1  17972  cnextcn  18051  tmdcn2  18072  psmettri  18295  isxmet2d  18310  xmettri  18334  xmetres2  18344  bldisj  18381  blss2ps  18386  blss2  18387  xmstri2  18449  mstri2  18450  xmstri  18451  mstri  18452  xmstri3  18453  mstri3  18454  msrtri  18455  comet  18496  met2ndci  18505  ngprcan  18609  ngplcan  18610  ngpsubcan  18613  nrgdsdi  18654  nrgdsdir  18655  nlmdsdi  18670  nlmdsdir  18671  blcvx  18782  iocopnst  18918  icccvx  18928  pi1grplem  19027  pi1xfrf  19031  pi1cof  19037  cphdivcl  19098  cphsubdir  19123  cphsubdi  19124  bcthlem5  19234  volfiniun  19394  volcn  19451  itg1val2  19529  dvconst  19756  dvlip  19830  ftc1a  19874  ulmdvlem3  20271  ang180  20609  cvxcl  20776  scvxcvx  20777  sgmmul  20938  logexprlim  20962  dchrabl  20991  isspthonpth  21537  wlkdvspth  21561  grpomuldivass  21790  grpopnpcan2  21794  grponpncan  21796  grpodiveq  21797  ablodivdiv4  21832  ablonnncan  21834  ismndo1  21885  nvsubadd  22089  dipdi  22297  dipsubdi  22303  disjdsct  24043  dvrdir  24179  dvrcan5  24182  kerf1hrm  24215  reofld  24233  pstmfval  24244  qqhval2lem  24318  qqhvq  24324  esumcvg  24429  sigaclcu  24453  measdivcstOLD  24531  measdivcst  24532  erdszelem9  24838  cvmseu  24916  colinearalglem1  25749  colinearalg  25753  axcgrtr  25758  axlowdimlem16  25800  axeuclidlem  25805  axcontlem4  25810  axcontlem7  25813  axcontlem12  25818  cgrid2  25841  btwncomim  25851  btwnswapid  25855  trisegint  25866  cgrxfr  25893  btwnxfr  25894  brofs2  25915  brifs2  25916  endofsegid  25923  btwnconn1lem11  25935  btwnconn2  25940  segcon2  25943  seglemin  25951  segletr  25952  btwnsegle  25955  colinbtwnle  25956  broutsideof2  25960  btwnoutside  25963  broutsideof3  25964  outsideoftr  25967  outsidele  25970  ellines  25990  linethrueu  25994  sdclem1  26337  sstotbnd2  26373  zerdivemp1x  26461  isdrngo2  26464  iscringd  26499  irrapxlem6  26780  jm2.26lem3  26962  mpaamn  27229  pmtrprfv  27264  psgnunilem3  27287  matrng  27348  matassa  27349  mendrng  27368  mendlmod  27369  mendassa  27370  rfcnpre4  27572  fmuldfeq  27580  stoweidlem43  27659  stoweidlem52  27668  stoweidlem53  27669  stoweidlem56  27672  swrdccatin2lem1  28017  usg2wotspth  28081  2pthwlkonot  28082  bnj970  29024  bnj910  29025  lsmsat  29491  lfladdcl  29554  lflnegcl  29558  lflvscl  29560  lshpkrlem4  29596  lshpkrlem6  29598  ldualgrplem  29628  lduallmodlem  29635  latmassOLD  29712  latm12  29713  latm32  29714  latmrot  29715  latmmdiN  29717  latmmdir  29718  omlfh1N  29741  omlfh3N  29742  cvrnbtwn2  29758  cvlexchb1  29813  cvlexch3  29815  cvlexch4N  29816  cvlatexchb1  29817  cvlsupr2  29826  hlatjass  29852  hlatj12  29853  hlatj32  29854  cvrat  29904  atcvrj0  29910  cvrat2  29911  atltcvr  29917  atexchltN  29923  cvrat3  29924  cvrat4  29925  atbtwnexOLDN  29929  atbtwnex  29930  3dimlem3  29943  3dimlem3OLDN  29944  3at  29972  2atneat  29997  llncmp  30004  2at0mat0  30007  2atmat0  30008  islpln2a  30030  llncvrlpln  30040  lplncmp  30044  3atnelvolN  30068  4atlem11  30091  lplncvrlvol  30098  lvolcmp  30099  2atm2atN  30267  elpaddatriN  30285  elpadd2at2  30289  paddasslem8  30309  paddasslem17  30318  paddass  30320  padd12N  30321  paddssw1  30325  pmodlem2  30329  pmodN  30332  pmapjlln1  30337  atmod1i2  30341  pexmidlem2N  30453  pexmidlem7N  30458  pl42lem2N  30462  pl42lem3N  30463  pl42lem4N  30464  pl42N  30465  lhp2lt  30483  lhpm0atN  30511  lautlt  30573  lautcvr  30574  lautj  30575  lautm  30576  ltrneq2  30630  cdleme1b  30708  cdleme3b  30711  cdleme3c  30712  cdleme9b  30734  cdlemefs27cl  30895  cdleme42mN  30969  cdlemg4c  31094  trljco  31222  tgrpgrplem  31231  tendoplass  31265  tendodi1  31266  tendodi2  31267  erngplus2  31286  erngplus2-rN  31294  cdlemk36  31395  erngdvlem3  31472  erngdvlem3-rN  31480  dvaplusgv  31492  tendospass  31502  tendospdi1  31503  dvalveclem  31508  dialss  31529  dvhvaddass  31580  dvhopvsca  31585  dvhlveclem  31591  diblss  31653  diclss  31676  diclspsn  31677  cdlemn11pre  31693  dihmeetlem12N  31801  dihmeetlem16N  31805  dihmeetlem17N  31806  dvh4dimN  31930  lpolsatN  31971  lpolpolsatN  31972  dochpolN  31973  lclkr  32016  lclkrs  32022  lcfr  32068
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  df-3an 938
  Copyright terms: Public domain W3C validator