Theorem negeqd 10275

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

Step	Hyp	Ref	Expression
1		negeqd.1	. 2 |- ( ph -> A = B )
2		negeq 10273	. 2 |- ( A = B -> -u A = -u B )
3	1, 2	syl 17	1 |- ( ph -> -u A = -u B )

Syntax hints:   -> wi 4   = wceq 1483   -ucneg 10267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269

This theorem is referenced by:  negdi  10338  mulneg2  10467  mulm1  10471  ltord2  10557  leord2  10558  eqord2  10559  divneg  10719  div2neg  10748  recgt0  10867  infrenegsup  11006  supminf  11775  mul2lt0rlt0  11932  ceilval  12639  dfceil2  12640  ceilid  12650  modcyc2  12706  monoord2  12832  expval  12862  discr  13001  reneg  13865  imneg  13873  cjcj  13880  cjneg  13887  sqeqd  13906  telfsumo2  14535  infcvgaux1i  14589  infcvgaux2i  14590  risefallfac  14755  bpoly3  14789  sinneg  14876  tanneg  14878  sincossq  14906  odd2np1  15065  oexpneg  15069  modgcd  15253  pcneg  15578  mulgval  17543  mulgneg  17560  psgnunilem2  17915  evth2  22759  ivth2  23224  mbfposb  23420  mbfinf  23432  mbfi1flimlem  23489  iblcnlem  23555  iblrelem  23557  itgrevallem1  23561  iblneg  23569  itgneg  23570  ibladd  23587  ditgeq1  23612  ditgeq2  23613  ditgeq3  23614  ditgneg  23621  ditgswap  23623  dvrec  23718  dvrecg  23736  dvmptdiv  23737  dvexp3  23741  dvsincos  23744  rolle  23753  dvivth  23773  dvfsumge  23785  dvfsumlem2  23790  dvfsum2  23797  ftc2ditg  23809  vieta1lem2  24066  vieta1  24067  aaliou3lem2  24098  aaliou3lem8  24100  aaliou3lem5  24102  aaliou3lem6  24103  aaliou3lem7  24104  aaliou3  24106  sinperlem  24232  efimpi  24243  ptolemy  24248  sineq0  24273  efeq1  24275  tanregt0  24285  efif1olem2  24289  lognegb  24336  logneg2  24361  advlogexp  24401  logtayl  24406  logtayl2  24408  logccv  24409  cxpmul2z  24437  logbrec  24520  cosangneg2d  24537  isosctrlem2  24549  isosctrlem3  24550  angpined  24557  dcubic1lem  24570  dcubic2  24571  mcubic  24574  cubic2  24575  dquart  24580  quart1lem  24582  quartlem1  24584  quart  24588  asinlem3a  24597  asinneg  24613  atanneg  24634  atancj  24637  atanlogaddlem  24640  atanlogsublem  24642  atantan  24650  atantayl  24664  birthdaylem3  24680  amgmlem  24716  emcllem7  24728  lgamgulmlem2  24756  ftalem5  24803  basellem5  24811  basellem9  24815  lgsneg1  25047  lgseisenlem1  25100  lgseisenlem4  25103  m1lgs  25113  2sqblem  25156  dchrisum0flblem1  25197  rpvmasum2  25201  pntrsumo1  25254  pntrlog2bndlem2  25267  pntibndlem2  25280  padicfval  25305  padicval  25306  ostth3  25327  brbtwn2  25785  colinearalglem4  25789  axsegconlem9  25805  ex-ceil  27305  nvabs  27527  ipasslem2  27687  numdenneg  29563  archirngz  29743  xrge0iifcv  29980  xrge0iifhom  29983  xrge0iif1  29984  xrge0tmdOLD  29991  xrge0tmd  29992  fdvneggt  30678  fdvnegge  30680  climlec3  31619  dvtan  33460  itg2addnclem3  33463  ibladdnc  33467  ftc1anclem5  33489  ftc1anclem6  33490  areacirclem1  33500  areacirc  33505  pellexlem6  37398  pell1234qrdich  37425  rmxm1  37499  rmym1  37500  monotoddzzfi  37507  monotoddzz  37508  oddcomabszz  37509  acongeq12d  37546  acongeq  37550  sineq0ALT  39173  infnsuprnmpt  39465  supminfrnmpt  39672  supminfxr  39694  neglimc  39879  dvcosax  40141  itgsin0pilem1  40165  itgsinexplem1  40169  itgsincmulx  40190  stoweidlem13  40230  stirlinglem5  40295  dirkerper  40313  dirkertrigeqlem3  40317  fourierdlem39  40363  fourierdlem40  40364  fourierdlem41  40365  fourierdlem43  40367  fourierdlem49  40372  fourierdlem73  40396  fourierdlem78  40401  fourierdlem103  40426  sqwvfourb  40446  etransclem46  40497  etransclem47  40498  sigarac  41041  sigaras  41044  sigarms  41045  sigariz  41052  sigarcol  41053  sharhght  41054  sigaradd  41055  2pwp1prm  41503  oexpnegALTV  41588  oexpnegnz  41589  amgmwlem  42548