Theorem negeqd 10883

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 10881	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝐴 = -𝐵)

Syntax hints:   → wi 4   = wceq 1536  -cneg 10874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162  df-neg 10876

This theorem is referenced by:  negdi  10946  mulneg2  11080  mulm1  11084  ltord2  11172  leord2  11173  eqord2  11174  divneg  11335  div2neg  11366  recgt0  11489  infrenegsup  11627  supminf  12338  mul2lt0rlt0  12494  ceilval  13211  dfceil2  13212  ceilid  13222  modcyc2  13278  monoord2  13404  expval  13434  discr  13604  reneg  14487  imneg  14495  cjcj  14502  cjneg  14509  sqeqd  14528  telfsumo2  15161  infcvgaux1i  15215  infcvgaux2i  15216  risefallfac  15381  bpoly3  15415  sinneg  15502  tanneg  15504  sincossq  15532  odd2np1  15693  oexpneg  15697  modgcd  15883  pcneg  16213  mulgval  18231  mulgneg  18249  psgnunilem2  18626  evth2  23567  ivth2  24059  mbfposb  24257  mbfinf  24269  mbfi1flimlem  24326  iblcnlem  24392  iblrelem  24394  itgrevallem1  24398  iblneg  24406  itgneg  24407  ibladd  24424  ditgeq1  24449  ditgeq2  24450  ditgeq3  24451  ditgneg  24458  ditgswap  24460  dvrec  24555  dvrecg  24573  dvmptdiv  24574  dvexp3  24578  dvsincos  24581  rolle  24590  dvivth  24610  dvfsumge  24622  dvfsumlem2  24627  dvfsum2  24634  ftc2ditg  24646  vieta1lem2  24903  vieta1  24904  aaliou3lem2  24935  aaliou3lem8  24937  aaliou3lem5  24939  aaliou3lem6  24940  aaliou3lem7  24941  aaliou3  24943  sinperlem  25069  efimpi  25080  ptolemy  25085  sineq0  25112  efeq1  25116  tanregt0  25126  efif1olem2  25130  lognegb  25176  logneg2  25201  advlogexp  25241  logtayl  25246  logtayl2  25248  logccv  25249  cxpmul2z  25277  logbrec  25363  cosangneg2d  25388  isosctrlem2  25400  isosctrlem3  25401  angpined  25411  dcubic1lem  25424  dcubic2  25425  mcubic  25428  cubic2  25429  dquart  25434  quart1lem  25436  quartlem1  25438  quart  25442  asinlem3a  25451  asinneg  25467  atanneg  25488  atancj  25491  atanlogaddlem  25494  atanlogsublem  25496  atantan  25504  atantayl  25518  birthdaylem3  25534  amgmlem  25570  emcllem7  25582  lgamgulmlem2  25610  ftalem5  25657  basellem5  25665  basellem9  25669  lgsneg1  25901  lgseisenlem1  25954  lgseisenlem4  25957  m1lgs  25967  2sqblem  26010  dchrisum0flblem1  26087  rpvmasum2  26091  pntrsumo1  26144  pntrlog2bndlem2  26157  pntibndlem2  26170  padicfval  26195  padicval  26196  ostth3  26217  brbtwn2  26694  colinearalglem4  26698  axsegconlem9  26714  ex-ceil  28230  nvabs  28452  ipasslem2  28612  numdenneg  30536  archirngz  30822  ccfldextdgrr  31061  xrge0iifcv  31181  xrge0iifhom  31184  xrge0iif1  31185  xrge0tmd  31192  xrge0tmdALT  31193  fdvneggt  31875  fdvnegge  31877  climlec3  32969  dvtan  34946  itg2addnclem3  34949  ibladdnc  34953  ftc1anclem5  34975  ftc1anclem6  34976  areacirclem1  34986  areacirc  34991  dffltz  39277  3cubeslem3r  39290  pellexlem6  39437  pell1234qrdich  39464  rmxm1  39537  rmym1  39538  monotoddzzfi  39545  monotoddzz  39546  oddcomabszz  39547  acongeq12d  39582  acongeq  39586  sineq0ALT  41277  infnsuprnmpt  41528  supminfrnmpt  41725  supminfxr  41746  neglimc  41934  dvcosax  42217  itgsin0pilem1  42241  itgsinexplem1  42245  itgsincmulx  42265  stoweidlem13  42305  stirlinglem5  42370  dirkerper  42388  dirkertrigeqlem3  42392  fourierdlem39  42438  fourierdlem40  42439  fourierdlem41  42440  fourierdlem43  42442  fourierdlem49  42447  fourierdlem73  42471  fourierdlem78  42476  fourierdlem103  42501  sqwvfourb  42521  etransclem46  42572  etransclem47  42573  sigarac  43116  sigaras  43119  sigarms  43120  sigariz  43127  sigarcol  43128  sharhght  43129  sigaradd  43130  2pwp1prm  43758  oexpnegALTV  43849  oexpnegnz  43850  itschlc0yqe  44754  itsclc0yqsol  44758  itsclquadb  44770  itscnhlinecirc02plem2  44777  amgmwlem  44910