Theorem negeqd 11454

Description: Equality deduction for negatives. (Contributed by NM, 14-May-1999.)

Hypothesis

Ref	Expression
negeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
negeqd	⊢ (𝜑 → -𝐴 = -𝐵)

Proof of Theorem negeqd

Step	Hyp	Ref	Expression
1		negeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		negeq 11452	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝐴 = -𝐵)

Syntax hints:   → wi 4   = wceq 1542  -cneg 11445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447

This theorem is referenced by:  negdi  11517  mulneg2  11651  mulm1  11655  ltord2  11743  leord2  11744  eqord2  11745  divneg  11906  div2neg  11937  recgt0  12060  infrenegsup  12197  supminf  12919  mul2lt0rlt0  13076  ceilval  13803  dfceil2  13804  ceilid  13816  modcyc2  13872  monoord2  13999  expval  14029  discr  14203  reneg  15072  imneg  15080  cjcj  15087  cjneg  15094  sqeqd  15113  telfsumo2  15749  infcvgaux1i  15803  infcvgaux2i  15804  risefallfac  15968  bpoly3  16002  sinneg  16089  tanneg  16091  sincossq  16119  odd2np1  16284  oexpneg  16288  modgcd  16474  pcneg  16807  mulgval  18954  mulgneg  18972  psgnunilem2  19363  evth2  24476  ivth2  24972  mbfposb  25170  mbfinf  25182  mbfi1flimlem  25240  iblcnlem  25306  iblrelem  25308  itgrevallem1  25312  iblneg  25320  itgneg  25321  ibladd  25338  ditgeq1  25365  ditgeq2  25366  ditgeq3  25367  ditgneg  25374  ditgswap  25376  dvrec  25472  dvrecg  25490  dvmptdiv  25491  dvexp3  25495  dvsincos  25498  rolle  25507  dvivth  25527  dvfsumge  25539  dvfsumlem2  25544  dvfsum2  25551  ftc2ditg  25563  vieta1lem2  25824  vieta1  25825  aaliou3lem2  25856  aaliou3lem8  25858  aaliou3lem5  25860  aaliou3lem6  25861  aaliou3lem7  25862  aaliou3  25864  sinperlem  25990  efimpi  26001  ptolemy  26006  sineq0  26033  efeq1  26037  tanregt0  26048  efif1olem2  26052  lognegb  26098  logneg2  26123  advlogexp  26163  logtayl  26168  logtayl2  26170  logccv  26171  cxpmul2z  26199  logbrec  26287  cosangneg2d  26312  isosctrlem2  26324  isosctrlem3  26325  angpined  26335  dcubic1lem  26348  dcubic2  26349  mcubic  26352  cubic2  26353  dquart  26358  quart1lem  26360  quartlem1  26362  quart  26366  asinlem3a  26375  asinneg  26391  atanneg  26412  atancj  26415  atanlogaddlem  26418  atanlogsublem  26420  atantan  26428  atantayl  26442  birthdaylem3  26458  amgmlem  26494  emcllem7  26506  lgamgulmlem2  26534  ftalem5  26581  basellem5  26589  basellem9  26593  lgsneg1  26825  lgseisenlem1  26878  lgseisenlem4  26881  m1lgs  26891  2sqblem  26934  dchrisum0flblem1  27011  rpvmasum2  27015  pntrsumo1  27068  pntrlog2bndlem2  27081  pntibndlem2  27094  padicfval  27119  padicval  27120  ostth3  27141  brbtwn2  28163  colinearalglem4  28167  axsegconlem9  28183  ex-ceil  29701  nvabs  29925  ipasslem2  30085  numdenneg  32023  archirngz  32335  ccfldextdgrr  32746  xrge0iifcv  32914  xrge0iifhom  32917  xrge0iif1  32918  xrge0tmd  32925  xrge0tmdALT  32926  fdvneggt  33612  fdvnegge  33614  climlec3  34703  gg-dvfsumlem2  35183  dvtan  36538  itg2addnclem3  36541  ibladdnc  36545  ftc1anclem5  36565  ftc1anclem6  36566  areacirclem1  36576  areacirc  36581  dffltz  41376  3cubeslem3r  41425  pellexlem6  41572  pell1234qrdich  41599  rmxm1  41673  rmym1  41674  monotoddzzfi  41681  monotoddzz  41682  oddcomabszz  41683  acongeq12d  41718  acongeq  41722  sineq0ALT  43698  infnsuprnmpt  43954  supminfrnmpt  44155  supminfxr  44174  neglimc  44363  dvcosax  44642  itgsin0pilem1  44666  itgsinexplem1  44670  itgsincmulx  44690  stoweidlem13  44729  stirlinglem5  44794  dirkerper  44812  dirkertrigeqlem3  44816  fourierdlem39  44862  fourierdlem40  44863  fourierdlem41  44864  fourierdlem43  44866  fourierdlem49  44871  fourierdlem73  44895  fourierdlem78  44900  fourierdlem103  44925  sqwvfourb  44945  etransclem46  44996  etransclem47  44997  sigarac  45568  sigaras  45571  sigarms  45572  sigariz  45579  sigarcol  45580  sharhght  45581  sigaradd  45582  2pwp1prm  46257  oexpnegALTV  46345  oexpnegnz  46346  itschlc0yqe  47446  itsclc0yqsol  47450  itsclquadb  47462  itscnhlinecirc02plem2  47469  amgmwlem  47849