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

Theorem simpr2 1001
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 995 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 464 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  simplr2  1037  simprr2  1043  simp1r2  1091  simp2r2  1097  simp3r2  1103  3anandis  1328  wereu  4789  isopolem  6142  fr3nr  6514  frfi  7680  intrnfi  7791  fisupcl  7842  cnfcomlem  8056  cnfcomlemOLD  8064  ackbij1lem15  8527  cofsmo  8562  sornom  8570  fpwwe2lem5  8923  dedekindle  9656  supmul1  10424  eluzuzle  11009  xlesubadd  11376  elioc2  11508  elico2  11509  elicc2  11510  fseq1p1m1  11674  fz0fzelfz0  11702  swrdsbslen  12584  swrdspsleq  12585  ccatswrd  12592  swrdswrdlem  12595  tanadd  13904  dvds2ln  14016  cshwsidrepsw  14580  ressress  14699  f1ovscpbl  14933  mreexexlem4d  15054  mreexexd  15055  iscatd2  15088  2oppccomf  15131  issubc3  15255  fthmon  15333  fuccocl  15370  fucidcl  15371  invfuc  15380  initoeu2lem0  15409  initoeu2lem1  15410  curf2cl  15617  yonedalem4c  15663  yonedalem3  15666  pospo  15720  latjle12  15809  latjlej1  15812  latnlej2  15818  latlem12  15825  latmlem1  15828  latledi  15836  latjass  15842  latj12  15843  latj32  15844  latj13  15845  latj31  15846  latjrot  15847  latjjdi  15850  latjjdir  15851  latdisdlem  15936  prdsmndd  16070  frmdmnd  16144  grpsubrcan  16236  grpsubadd  16243  grpaddsubass  16245  grpsubsub4  16248  grppnpcan2  16249  grpnpncan  16250  mulgnndir  16281  mulgnn0dir  16282  mulgdir  16284  mulgnnass  16287  mulgnn0ass  16288  mulgass  16289  mulgsubdir  16290  pwsmulg  16301  issubg2  16333  eqgval  16367  qusgrp  16373  galcan  16459  gacan  16460  oppgmnd  16506  symggrp  16542  fvcosymgeq  16571  pmtrprfv  16595  psgnunilem3  16638  cmn32  16933  cmn12  16935  abladdsub  16942  mulgdi  16952  mulgsubdi  16955  dprdss  17189  dprdz  17190  dprdf1o  17192  dprdsn  17196  dprd2da  17204  dmdprdsplit  17209  ablfac1b  17234  pgpfac1lem5  17243  srgi  17276  srgbinom  17309  ringi  17324  prdsringd  17374  opprring  17393  mulgass3  17399  dvrass  17452  subrgunit  17560  issubrg2  17562  abvdiv  17599  lsssn0  17707  islss3  17718  prdslmodd  17728  islmhm2  17797  lspsolv  17902  islbs2  17913  islbs3  17914  lbsextlem4  17920  sralmod  17946  issubassa  18086  sraassa  18087  psrbaglesupp  18130  psrbaglesuppOLD  18131  psrbaglecl  18132  psrbagcon  18135  psrgrp  18164  psrlmod  18167  psrring  18179  psrassa  18182  psgndiflemB  18727  ipdir  18765  ipdi  18766  ipsubdir  18768  ipsubdi  18769  ipass  18771  ipassr  18772  ipassr2  18773  isphld  18780  ocvlss  18794  mamudm  18975  matring  19030  matassa  19031  ofco2  19038  ma1repveval  19158  mdetunilem1  19199  mdetunilem9  19207  chpscmatgsumbin  19430  iinopn  19496  restopnb  19762  subbascn  19841  nrmsep2  19943  isnrm3  19946  regsep2  19963  dnsconst  19965  dfcon2  20005  1stcelcls  20047  dislly  20083  ptuni2  20162  tx1stc  20236  0nelfb  20417  infil  20449  fsubbas  20453  filssufilg  20497  hauspwpwf1  20573  cnextcn  20652  tmdcn2  20673  ustuqtoplem  20827  utopsnneiplem  20835  psmettri  20900  isxmet2d  20915  xmettri  20939  xmetres2  20949  bldisj  20986  blss2ps  20991  blss2  20992  xmstri2  21054  mstri2  21055  xmstri  21056  mstri  21057  xmstri3  21058  mstri3  21059  msrtri  21060  comet  21101  stdbdbl  21105  met2ndci  21110  ngprcan  21214  ngplcan  21215  ngpsubcan  21218  nrgdsdi  21259  nrgdsdir  21260  nlmdsdi  21275  nlmdsdir  21276  blcvx  21388  icoopnst  21524  pi1grplem  21634  cvsdiv  21694  cvsdivcl  21695  cphdivcl  21714  cphsubdir  21739  cphsubdi  21740  tchcph  21765  bcthlem5  21852  volfiniun  22042  volcn  22100  itg1val2  22176  dvconst  22405  dvlip  22479  ftc1a  22523  ulmval  22860  ulmdvlem3  22882  ang180  23264  cvxcl  23431  scvxcvx  23432  sgmmul  23593  dchrabl  23646  motgrp  24050  f1otrge  24296  colinearalglem1  24330  axcgrtr  24339  axeuclidlem  24386  axcontlem3  24390  axcontlem4  24391  axcontlem7  24394  eengtrkg  24409  eengtrkge  24410  isspthonpth  24707  wlkdvspth  24731  clwlkfoclwwlk  24966  el2spthonot0  24992  el2wlkonotot0  24993  usg2wotspth  25005  2spontn0vne  25008  rusgranumwlks  25077  rusgranumwwlkg  25080  iseupa  25086  3vfriswmgra  25126  frgrareggt1  25237  grpomuldivass  25368  grponpncan  25374  grpodiveq  25375  ablomuldiv  25408  ablodivdiv4  25410  ablonnncan1  25414  nvmdi  25662  nvsubadd  25667  dipassr  25878  archiabllem2c  27892  dvrdir  27934  dvrcan5  27937  reofld  27984  pstmfval  28029  qqhval2lem  28115  qqhvq  28121  measdivcstOLD  28351  measdivcst  28352  carsggect  28445  erdszelem9  28832  rescon  28880  cvmseu  28910  cvmlift2lem10  28946  cvmlift2lem12  28948  elmrsubrn  29069  mclsind  29119  frrlem4  29555  cgrid2  29806  segconeu  29814  btwncomim  29816  btwnswapid  29820  trisegint  29831  cgrxfr  29858  brofs2  29880  endofsegid  29888  btwnconn2  29905  seglemin  29916  segletr  29917  btwnsegle  29920  colinbtwnle  29921  broutsideof2  29925  btwnoutside  29928  broutsideof3  29929  outsideoftr  29932  outsidele  29935  fvray  29944  fvline  29947  ellines  29955  ftc1anc  30264  sdclem1  30402  sstotbnd2  30436  iscringd  30562  irrapxlem6  30928  jm2.26lem3  31109  dgrsub2  31252  mpaaroot  31272  mendring  31309  mendlmod  31310  mendassa  31311  rfcnpre3  31575  fmuldfeq  31743  stoweidlem43  31991  stoweidlem52  32000  stoweidlem53  32001  stoweidlem56  32004  stoweidlem57  32005  stoweidlem60  32008  ltsubsubaddltsub  32645  copissgrp  32814  cznrng  32963  funcringcsetcALTV2lem9  33052  funcringcsetclem9ALTV  33075  ldepsprlem  33273  lincresunit3  33282  lincreslvec3  33283  bnj1098  34189  bnj149  34280  bnj1118  34387  lsmsat  35146  lfladdcl  35209  lflnegcl  35213  lflvscl  35215  eqlkr  35237  lshpkrlem4  35251  lshpkrlem6  35253  ldualgrplem  35283  lduallmodlem  35290  latmassOLD  35367  latm12  35368  latm32  35369  latmrot  35370  latmmdiN  35372  latmmdir  35373  omlfh1N  35396  omlfh3N  35397  cvrnbtwn2  35413  cvlexchb1  35468  cvlsupr2  35481  hlatjass  35507  hlatj12  35508  hlatj32  35509  cvrat  35559  cvrat2  35566  atltcvr  35572  atexchltN  35578  cvrat3  35579  cvrat4  35580  atbtwnexOLDN  35584  atbtwnex  35585  3dimlem3  35598  3dimlem3OLDN  35599  3at  35627  2atneat  35652  llncmp  35659  2at0mat0  35662  2atmat0  35663  llncvrlpln  35695  lplncmp  35699  2llnjaN  35703  4atlem11  35746  lplncvrlvol  35753  lvolcmp  35754  2atm2atN  35922  elpaddatriN  35940  paddasslem8  35964  paddass  35975  padd12N  35976  paddssw2  35981  paddss  35982  pmod1i  35985  pmodN  35987  pmapjlln1  35992  atmod1i1  35994  atmod1i2  35996  pexmidlem2N  36108  pl42lem2N  36117  pl42lem3N  36118  pl42lem4N  36119  pl42N  36120  lhpm0atN  36166  lautlt  36228  lautcvr  36229  lautj  36230  lautm  36231  ltrneq2  36285  cdlemd1  36336  cdleme1b  36364  cdleme1  36365  cdleme2  36366  cdleme3e  36370  cdlemefr27cl  36542  cdlemefs27cl  36552  cdleme42ke  36624  cdleme42mN  36626  cdlemf2  36701  cdlemftr2  36705  trljco  36879  tgrpgrplem  36888  tendoplass  36922  tendodi1  36923  tendodi2  36924  cdlemk34  37049  cdlemk36  37052  erngdvlem3-rN  37137  tendospdi1  37160  dialss  37186  dvhvaddass  37237  dvhopvsca  37242  dvhlveclem  37248  diblss  37310  diclss  37333  diclspsn  37334  cdlemn11pre  37350  dihmeetlem12N  37458  dihmeetlem16N  37462  dihmeetlem17N  37463  dihmeetlem18N  37464  dvh4dimN  37587  lpolconN  37627  dochpolN  37630  lclkr  37673  lclkrs  37679  lcfr  37725  iunrelexpmin2  38226  relexpxpmin  38244  relexpmulg  38246
  Copyright terms: Public domain W3C validator