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

Theorem simpr3 996
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 990 . 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 965
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 967
This theorem is referenced by:  simplr3  1032  simprr3  1038  simp1r3  1086  simp2r3  1092  simp3r3  1098  3anandis  1321  isopolem  6148  fr3nr  6504  suppfnss  6827  elfir  7779  intrnfi  7780  fisupcl  7831  cnfcomlem  8046  cnfcomlemOLD  8054  ackbij1lem15  8517  pwfseqlem4a  8942  pwfseqlem4  8943  xlesubadd  11340  elioc2  11472  elico2  11473  elicc2  11474  fseq1p1m1  11654  swrdsymbeq  12462  ccatswrd  12471  tanadd  13572  dvds2ln  13684  cshwsidrepsw  14241  ressress  14357  f1ovscpbl  14586  mreexexlem4d  14707  mreexexd  14708  2oppccomf  14786  fthmon  14959  fuccocl  14996  fucidcl  14997  invfuc  15006  curf2cl  15163  yonedalem4c  15209  yonedalem3  15212  pospo  15265  latjle12  15354  latjlej1  15357  latnlej2  15363  latlem12  15370  latmlem1  15373  latledi  15381  latjass  15387  latj12  15388  latj32  15389  latj13  15390  latj31  15391  latjrot  15392  latjjdi  15395  latjjdir  15396  latdisdlem  15481  prdsmndd  15576  imasmnd2  15580  imasmnd  15581  frmdmnd  15659  grpsubadd  15735  grpaddsubass  15737  grpsubsub4  15740  grppnpcan2  15741  grpnpncan  15742  grpnnncan2  15743  mulgnndir  15771  mulgnn0dir  15772  mulgnnass  15777  mulgnn0ass  15778  mulgass  15779  pwsmulg  15791  imasgrp2  15792  imasgrp  15793  issubg2  15818  divsgrp  15858  galcan  15944  gacan  15945  oppgmnd  15991  symggrp  16027  pmtrprfv  16081  pmtr3ncom  16103  psgnunilem3  16124  frgp0  16381  cmn32  16419  cmn12  16421  abladdsub  16428  mulgdi  16438  mulgsubdi  16441  dprdss  16651  dprdf1o  16654  dprdsn  16658  dmdprdsplit  16671  pgpfac1lem5  16705  srgi  16738  rngi  16783  prdsrngd  16830  imasrng  16837  opprrng  16849  mulgass3  16855  dvrass  16908  kerf1hrm  16957  subrgunit  17009  issubrg2  17011  abvdiv  17048  lss1  17146  lsssn0  17155  islss3  17166  prdslmodd  17176  islmhm2  17245  lspsolv  17350  lbsextlem4  17368  sralmod  17394  issubassa  17521  sraassa  17522  psrbaglesupp  17561  psrbaglesuppOLD  17562  psrbagcon  17566  psrgrp  17595  psrlmod  17598  psrrng  17610  psrassa  17613  mpllsslem  17638  mpllsslemOLD  17640  ipdi  18197  ipsubdir  18199  ipsubdi  18200  ipassr  18203  ipassr2  18204  isphld  18211  ocvlss  18225  mamudm  18416  matrng  18459  matassa  18460  ofco2  18462  ma1repveval  18512  mdetunilem1  18553  mdetunilem9  18561  iinopn  18650  restopnb  18914  subbascn  18993  nrmsep2  19095  isnrm3  19098  t1sep  19109  regsep2  19115  dnsconst  19117  dfcon2  19158  dislly  19236  tx1stc  19358  qtophmeo  19525  filss  19561  infil  19571  fsubbas  19575  filssufilg  19619  hauspwpwf1  19695  cnextcn  19774  tmdcn2  19795  psmettri  20022  isxmet2d  20037  xmettri  20061  xmetres2  20071  bldisj  20108  blss2ps  20113  blss2  20114  xmstri2  20176  mstri2  20177  xmstri  20178  mstri  20179  xmstri3  20180  mstri3  20181  msrtri  20182  comet  20223  met2ndci  20232  ngprcan  20336  ngplcan  20337  ngpsubcan  20340  nrgdsdi  20381  nrgdsdir  20382  nlmdsdi  20397  nlmdsdir  20398  blcvx  20510  iocopnst  20647  icccvx  20657  pi1grplem  20756  pi1xfrf  20760  pi1cof  20766  cvsdiv  20816  cvsdivcl  20817  cphdivcl  20836  cphsubdir  20861  cphsubdi  20862  bcthlem5  20974  rrxcph  21031  volfiniun  21164  volcn  21222  itg1val2  21298  dvconst  21527  dvlip  21601  ftc1a  21645  ulmdvlem3  22003  ang180  22346  cvxcl  22514  scvxcvx  22515  sgmmul  22676  logexprlim  22700  dchrabl  22729  f1otrge  23290  xmstrkgc  23304  colinearalglem1  23324  colinearalg  23328  axcgrtr  23333  axlowdimlem16  23375  axeuclidlem  23380  axcontlem4  23385  axcontlem7  23388  axcontlem12  23393  eengtrkg  23403  eengtrkge  23404  isspthonpth  23655  wlkdvspth  23679  grpomuldivass  23908  grpopnpcan2  23912  grponpncan  23914  grpodiveq  23915  ablodivdiv4  23950  ablonnncan  23952  ismndo1  24003  nvsubadd  24207  dipdi  24415  dipsubdi  24421  disjdsct  26169  omndmul2  26340  archiabllem2c  26377  dvrdir  26423  dvrcan5  26426  reofld  26473  pstmfval  26488  qqhval2lem  26575  qqhvq  26581  esumcvg  26700  sigaclcu  26725  measdivcstOLD  26803  measdivcst  26804  erdszelem9  27251  cvmseu  27329  cgrid2  28198  btwncomim  28208  btwnswapid  28212  trisegint  28223  cgrxfr  28250  btwnxfr  28251  brofs2  28272  brifs2  28273  endofsegid  28280  btwnconn1lem11  28292  btwnconn2  28297  segcon2  28300  seglemin  28308  segletr  28309  btwnsegle  28312  colinbtwnle  28313  broutsideof2  28317  btwnoutside  28320  broutsideof3  28321  outsideoftr  28324  outsidele  28327  ellines  28347  linethrueu  28351  ftc1anc  28643  sdclem1  28807  sstotbnd2  28841  zerdivemp1x  28929  isdrngo2  28932  iscringd  28967  irrapxlem6  29336  jm2.26lem3  29518  mpaamn  29681  mendrng  29717  mendlmod  29718  mendassa  29719  rfcnpre4  29924  fmuldfeq  29932  stoweidlem43  30006  stoweidlem52  30015  stoweidlem53  30016  stoweidlem56  30019  modfsummods  30412  usg2wotspth  30571  2pthwlkonot  30572  rusgranumwwlkg  30745  numclwwlk5  30873  friendship  30883  linccl  31100  lincsumscmcl  31119  lincresunit3lem1  31165  monmatcollpw  31286  bnj970  32292  bnj910  32293  lsmsat  33011  lfladdcl  33074  lflnegcl  33078  lflvscl  33080  lshpkrlem4  33116  lshpkrlem6  33118  ldualgrplem  33148  lduallmodlem  33155  latmassOLD  33232  latm12  33233  latm32  33234  latmrot  33235  latmmdiN  33237  latmmdir  33238  omlfh1N  33261  omlfh3N  33262  cvrnbtwn2  33278  cvlexchb1  33333  cvlexch3  33335  cvlexch4N  33336  cvlatexchb1  33337  cvlsupr2  33346  hlatjass  33372  hlatj12  33373  hlatj32  33374  cvrat  33424  atcvrj0  33430  cvrat2  33431  atltcvr  33437  atexchltN  33443  cvrat3  33444  cvrat4  33445  atbtwnexOLDN  33449  atbtwnex  33450  3dimlem3  33463  3dimlem3OLDN  33464  3at  33492  2atneat  33517  llncmp  33524  2at0mat0  33527  2atmat0  33528  islpln2a  33550  llncvrlpln  33560  lplncmp  33564  3atnelvolN  33588  4atlem11  33611  lplncvrlvol  33618  lvolcmp  33619  2atm2atN  33787  elpaddatriN  33805  elpadd2at2  33809  paddasslem8  33829  paddasslem17  33838  paddass  33840  padd12N  33841  paddssw1  33845  pmodlem2  33849  pmodN  33852  pmapjlln1  33857  atmod1i2  33861  pexmidlem2N  33973  pexmidlem7N  33978  pl42lem2N  33982  pl42lem3N  33983  pl42lem4N  33984  pl42N  33985  lhp2lt  34003  lhpm0atN  34031  lautlt  34093  lautcvr  34094  lautj  34095  lautm  34096  ltrneq2  34150  cdleme1b  34228  cdleme3b  34231  cdleme3c  34232  cdleme9b  34254  cdlemefs27cl  34415  cdleme42mN  34489  cdlemg4c  34614  trljco  34742  tgrpgrplem  34751  tendoplass  34785  tendodi1  34786  tendodi2  34787  erngplus2  34806  erngplus2-rN  34814  cdlemk36  34915  erngdvlem3  34992  erngdvlem3-rN  35000  dvaplusgv  35012  tendospass  35022  tendospdi1  35023  dvalveclem  35028  dialss  35049  dvhvaddass  35100  dvhopvsca  35105  dvhlveclem  35111  diblss  35173  diclss  35196  diclspsn  35197  cdlemn11pre  35213  dihmeetlem12N  35321  dihmeetlem16N  35325  dihmeetlem17N  35326  dvh4dimN  35450  lpolsatN  35491  lpolpolsatN  35492  dochpolN  35493  lclkr  35536  lclkrs  35542  lcfr  35588
  Copyright terms: Public domain W3C validator