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

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

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 958 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 453 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simplr2  1000  simprr2  1006  simp1r2  1054  simp2r2  1060  simp3r2  1066  3anandis  1285  wereu  4538  fr3nr  4719  isopolem  6024  frfi  7311  intrnfi  7379  fisupcl  7428  cnfcomlem  7612  ackbij1lem15  8070  cofsmo  8105  sornom  8113  fpwwe2lem5  8465  supmul1  9929  xlesubadd  10798  elioc2  10929  elico2  10930  elicc2  10931  fseq1p1m1  11077  ccatswrd  11728  tanadd  12723  dvds2ln  12835  ressress  13481  f1ovscpbl  13706  mreexexlem4d  13827  mreexexd  13828  iscatd2  13861  2oppccomf  13906  issubc3  14001  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  frmdmnd  14759  grpsubrcan  14825  grpsubadd  14831  grpaddsubass  14833  grpsubsub4  14836  grppnpcan2  14837  grpnpncan  14838  mulgnndir  14867  mulgnn0dir  14868  mulgdir  14870  mulgnnass  14873  mulgnn0ass  14874  mulgass  14875  mulgsubdir  14876  pwsmulg  14887  issubg2  14914  eqgval  14944  divsgrp  14950  galcan  15036  gacan  15037  symggrp  15058  oppgmnd  15105  cmn32  15385  cmn12  15387  abladdsub  15394  mulgdi  15404  mulgsubdi  15407  dprdss  15542  dprdz  15543  dprdf1o  15545  dprdsn  15549  dprd2da  15555  dmdprdsplit  15560  ablfac1b  15583  pgpfac1lem5  15592  rngi  15631  prdsrngd  15673  opprrng  15691  mulgass3  15697  dvrass  15750  subrgunit  15841  issubrg2  15843  abvdiv  15880  lsssn0  15979  islss3  15990  prdslmodd  16000  islmhm2  16069  lspsolv  16170  islbs2  16181  islbs3  16182  lbsextlem4  16188  sralmod  16213  issubassa  16338  sraassa  16339  psrbaglesupp  16388  psrbaglecl  16389  psrbagcon  16391  psrgrp  16417  psrlmod  16420  psrrng  16429  psrassa  16432  ipdir  16825  ipdi  16826  ipsubdir  16828  ipsubdi  16829  ipass  16831  ipassr  16832  ipassr2  16833  isphld  16840  ocvlss  16854  iinopn  16930  restopnb  17193  subbascn  17272  nrmsep2  17374  isnrm3  17377  regsep2  17394  dnsconst  17396  dfcon2  17435  1stcelcls  17477  dislly  17513  ptuni2  17561  tx1stc  17635  0nelfb  17816  infil  17848  fsubbas  17852  filssufilg  17896  hauspwpwf1  17972  cnextcn  18051  tmdcn2  18072  ustuqtoplem  18222  utopsnneiplem  18230  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  stdbdbl  18500  met2ndci  18505  ngprcan  18609  ngplcan  18610  ngpsubcan  18613  nrgdsdi  18654  nrgdsdir  18655  nlmdsdi  18670  nlmdsdir  18671  blcvx  18782  icoopnst  18917  pi1grplem  19027  cphdivcl  19098  cphsubdir  19123  cphsubdi  19124  tchcph  19147  bcthlem5  19234  volfiniun  19394  volcn  19451  itg1val2  19529  dvconst  19756  dvlip  19830  ftc1a  19874  ulmval  20249  ulmdvlem3  20271  ang180  20609  cvxcl  20776  scvxcvx  20777  sgmmul  20938  dchrabl  20991  isspthonpth  21537  wlkdvspth  21561  iseupa  21640  grpomuldivass  21790  grponpncan  21796  grpodiveq  21797  ablomuldiv  21830  ablodivdiv4  21832  ablonnncan1  21836  nvmdi  22084  nvsubadd  22089  dipassr  22300  dvrdir  24179  dvrcan5  24182  reofld  24233  pstmfval  24244  qqhval2lem  24318  qqhvq  24324  measdivcstOLD  24531  measdivcst  24532  erdszelem9  24838  rescon  24886  cvmseu  24916  cvmlift2lem10  24952  cvmlift2lem12  24954  dedekindle  25141  frrlem4  25498  colinearalglem1  25749  axcgrtr  25758  axeuclidlem  25805  axcontlem3  25809  axcontlem4  25810  axcontlem7  25813  cgrid2  25841  segconeu  25849  btwncomim  25851  btwnswapid  25855  trisegint  25866  cgrxfr  25893  brofs2  25915  endofsegid  25923  btwnconn2  25940  seglemin  25951  segletr  25952  btwnsegle  25955  colinbtwnle  25956  broutsideof2  25960  btwnoutside  25963  broutsideof3  25964  outsideoftr  25967  outsidele  25970  fvray  25979  fvline  25982  ellines  25990  sdclem1  26337  sstotbnd2  26373  iscringd  26499  irrapxlem6  26780  jm2.26lem3  26962  dgrsub2  27207  mpaaroot  27228  pmtrprfv  27264  psgnunilem3  27287  matrng  27348  matassa  27349  mendrng  27368  mendlmod  27369  mendassa  27370  rfcnpre3  27571  fmuldfeq  27580  stoweidlem43  27659  stoweidlem52  27668  stoweidlem53  27669  stoweidlem56  27672  stoweidlem57  27673  stoweidlem60  27676  swrdswrdlem  28010  el2spthonot0  28068  usg2wotspth  28081  2spontn0vne  28084  3vfriswmgra  28109  bnj1098  28860  bnj149  28952  bnj1118  29059  lsmsat  29491  lfladdcl  29554  lflnegcl  29558  lflvscl  29560  eqlkr  29582  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  cvlsupr2  29826  hlatjass  29852  hlatj12  29853  hlatj32  29854  cvrat  29904  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  llncvrlpln  30040  lplncmp  30044  2llnjaN  30048  4atlem11  30091  lplncvrlvol  30098  lvolcmp  30099  2atm2atN  30267  elpaddatriN  30285  paddasslem8  30309  paddass  30320  padd12N  30321  paddssw2  30326  paddss  30327  pmod1i  30330  pmodN  30332  pmapjlln1  30337  atmod1i1  30339  atmod1i2  30341  pexmidlem2N  30453  pl42lem2N  30462  pl42lem3N  30463  pl42lem4N  30464  pl42N  30465  lhpm0atN  30511  lautlt  30573  lautcvr  30574  lautj  30575  lautm  30576  ltrneq2  30630  cdlemd1  30680  cdleme1b  30708  cdleme1  30709  cdleme2  30710  cdleme3e  30714  cdlemefr27cl  30885  cdlemefs27cl  30895  cdleme42ke  30967  cdleme42mN  30969  cdlemf2  31044  cdlemftr2  31048  trljco  31222  tgrpgrplem  31231  tendoplass  31265  tendodi1  31266  tendodi2  31267  cdlemk34  31392  cdlemk36  31395  erngdvlem3-rN  31480  tendospdi1  31503  dialss  31529  dvhvaddass  31580  dvhopvsca  31585  dvhlveclem  31591  diblss  31653  diclss  31676  diclspsn  31677  cdlemn11pre  31693  dihmeetlem12N  31801  dihmeetlem16N  31805  dihmeetlem17N  31806  dihmeetlem18N  31807  dvh4dimN  31930  lpolconN  31970  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