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

Theorem negeqd 9256
Description: Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
Hypothesis
Ref Expression
negeqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
negeqd  |-  ( ph  -> 
-u A  =  -u B )

Proof of Theorem negeqd
StepHypRef Expression
1 negeqd.1 . 2  |-  ( ph  ->  A  =  B )
2 negeq 9254 . 2  |-  ( A  =  B  ->  -u A  =  -u B )
31, 2syl 16 1  |-  ( ph  -> 
-u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   -ucneg 9248
This theorem is referenced by:  negdi  9314  mulneg2  9427  mulm1  9431  ltord2  9512  leord2  9513  eqord2  9514  divneg  9665  div2neg  9693  recgt0  9810  infmsup  9942  supminf  10519  modcyc2  11232  monoord2  11309  expval  11339  discr  11471  reneg  11885  imneg  11893  cjcj  11900  cjneg  11907  sqeqd  11926  fsumtscopo2  12537  infcvgaux1i  12591  infcvgaux2i  12592  sinneg  12702  tanneg  12704  sincossq  12732  odd2np1  12863  oexpneg  12866  modgcd  12991  pcneg  13202  mulgval  14847  mulgneg  14863  evth2  18938  ivth2  19305  mbfposb  19498  mbfinf  19510  mbfi1flimlem  19567  iblcnlem  19633  iblrelem  19635  itgrevallem1  19639  iblneg  19647  itgneg  19648  ibladd  19665  ditgeq1  19688  ditgeq2  19689  ditgeq3  19690  ditgneg  19697  ditgswap  19699  dvrec  19794  dvexp3  19815  dvsincos  19818  rolle  19827  dvivth  19847  dvfsumge  19859  dvfsumlem2  19864  dvfsum2  19871  ftc2ditg  19883  vieta1lem2  20181  vieta1  20182  aaliou3lem2  20213  aaliou3lem8  20215  aaliou3lem5  20217  aaliou3lem6  20218  aaliou3lem7  20219  aaliou3  20221  sinperlem  20341  efimpi  20352  ptolemy  20357  sineq0  20382  efeq1  20384  tanregt0  20394  efif1olem2  20398  lognegb  20437  logneg2  20463  advlogexp  20499  logtayl  20504  logtayl2  20506  logccv  20507  cxpmul2z  20535  cosangneg2d  20602  isosctrlem2  20616  isosctrlem3  20617  angpined  20624  dcubic1lem  20636  dcubic2  20637  mcubic  20640  cubic2  20641  dquart  20646  quart1lem  20648  quartlem1  20650  quart  20654  asinlem3a  20663  asinneg  20679  atanneg  20700  atancj  20703  atanlogaddlem  20706  atanlogsublem  20708  atantan  20716  atantayl  20730  birthdaylem3  20745  amgmlem  20781  emcllem7  20793  ftalem5  20812  basellem5  20820  basellem9  20824  lgsneg1  21057  lgseisenlem1  21086  lgseisenlem4  21089  m1lgs  21099  2sqblem  21114  dchrisum0flblem1  21155  rpvmasum2  21159  pntrsumo1  21212  pntrlog2bndlem2  21225  pntibndlem2  21238  padicfval  21263  padicval  21264  ostth3  21285  nvabs  22115  ipasslem2  22286  numdenneg  24113  xrge0iifcv  24273  xrge0iifhom  24276  xrge0iif1  24277  xrge0tmdOLD  24284  xrge0tmd  24285  logbrec  24358  lgamgulmlem2  24767  climlec3  25167  risefallfac  25292  brbtwn2  25748  colinearalglem4  25752  axsegconlem9  25768  bpoly3  26008  itg2addnclem3  26157  ibladdnc  26161  areacirclem2  26181  areacirc  26187  pellexlem6  26787  pell1234qrdich  26814  rmxm1  26887  rmym1  26888  monotoddzzfi  26895  monotoddzz  26896  oddcomabszz  26897  acongeq12d  26934  acongeq  26938  psgnunilem2  27286  itgsin0pilem1  27611  itgsinexplem1  27615  stoweidlem13  27629  stirlinglem5  27694  sigarac  27709  sigaras  27712  sigarms  27713  sigariz  27720  sigarcol  27721  sharhght  27722  sigaradd  27723  ceilingval  28242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-neg 9250
  Copyright terms: Public domain W3C validator