Theorem negeqd 11451

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

Syntax hints:   → wi 4   = wceq 1567  -cneg 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-neg 11444

This theorem is referenced by:  negdi  11515  mulneg2  11651  mulm1  11655  ltord2  11743  leord2  11744  eqord2  11745  divneg  11906  div2neg  11938  recgt0  12061  infrenegsup  12198  supminf  12959  mul2lt0rlt0  13120  ceilval  13871  dfceil2  13872  ceilid  13884  modcyc2  13940  monoord2  14069  expval  14099  discr  14276  reneg  15176  imneg  15184  cjcj  15191  cjneg  15198  sqeqd  15217  telfsumo2  15855  infcvgaux1i  15911  infcvgaux2i  15912  risefallfac  16078  bpoly3  16112  sinneg  16202  tanneg  16204  sincossq  16232  odd2np1  16399  oexpneg  16403  modgcd  16590  pcneg  16934  mulgval  19137  mulgneg  19158  psgnunilem2  19565  evth2  25088  ivth2  25583  mbfposb  25781  mbfinf  25793  mbfi1flimlem  25850  iblcnlem  25917  iblrelem  25919  itgrevallem1  25923  iblneg  25931  itgneg  25932  ibladd  25949  ditgeq1  25976  ditgeq2  25977  ditgeq3  25978  ditgneg  25985  ditgswap  25987  dvrec  26083  dvrecg  26101  dvmptdiv  26102  dvexp3  26106  dvsincos  26109  rolle  26118  dvivth  26138  dvfsumge  26150  dvfsumlem2  26155  dvfsum2  26162  ftc2ditg  26174  vieta1lem2  26441  vieta1  26442  aaliou3lem2  26473  aaliou3lem8  26475  aaliou3lem5  26477  aaliou3lem6  26478  aaliou3lem7  26479  aaliou3  26481  sinperlem  26611  efimpi  26622  ptolemy  26627  sineq0  26655  efeq1  26659  tanregt0  26670  efif1olem2  26674  lognegb  26721  logneg2  26746  advlogexp  26786  logtayl  26791  logtayl2  26793  logccv  26794  cxpmul2z  26822  logbrec  26913  cosangneg2d  26938  isosctrlem2  26950  isosctrlem3  26951  angpined  26961  dcubic1lem  26974  dcubic2  26975  mcubic  26978  cubic2  26979  dquart  26984  quart1lem  26986  quartlem1  26988  quart  26992  asinlem3a  27001  asinneg  27017  atanneg  27038  atancj  27041  atanlogaddlem  27044  atanlogsublem  27046  atantan  27054  atantayl  27068  birthdaylem3  27084  amgmlem  27120  emcllem7  27132  lgamgulmlem2  27160  ftalem5  27207  basellem5  27215  basellem9  27219  lgsneg1  27452  lgseisenlem1  27505  lgseisenlem4  27508  m1lgs  27518  2sqblem  27561  dchrisum0flblem1  27638  rpvmasum2  27642  pntrsumo1  27695  pntrlog2bndlem2  27708  pntibndlem2  27721  padicfval  27746  padicval  27747  ostth3  27768  brbtwn2  29196  colinearalglem4  29200  axsegconlem9  29216  ex-ceil  30740  nvabs  30965  ipasslem2  31125  sgnval2  33021  re0cj  33029  argcj  33034  numdenneg  33100  archirngz  33450  elrgspnlem1  33503  ccfldextdgrr  34007  constrrtcc  34070  constrnegcl  34098  constrrecl  34104  cos9thpiminplylem1  34117  cos9thpiminplylem2  34118  xrge0iifcv  34269  xrge0iifhom  34272  xrge0iif1  34273  xrge0tmd  34280  xrge0tmdALT  34281  fdvneggt  34932  fdvnegge  34934  climlec3  36159  ditgeq123dv  36656  cbvditgdavw  36717  cbvditgdavw2  36733  dvtan  38243  itg2addnclem3  38246  ibladdnc  38250  ftc1anclem5  38270  ftc1anclem6  38271  areacirclem1  38281  areacirc  38286  25or6to4  42897  dffltz  43292  3cubeslem3r  43344  pellexlem6  43487  pell1234qrdich  43514  rmxm1  43587  rmym1  43588  monotoddzzfi  43595  monotoddzz  43596  oddcomabszz  43597  acongeq12d  43632  acongeq  43636  sineq0ALT  45571  infnsuprnmpt  45891  supminfrnmpt  46085  supminfxr  46104  neglimc  46287  dvcosax  46566  itgsin0pilem1  46590  itgsinexplem1  46594  itgsincmulx  46614  stoweidlem13  46653  stirlinglem5  46718  dirkerper  46736  dirkertrigeqlem3  46740  fourierdlem39  46786  fourierdlem40  46787  fourierdlem41  46788  fourierdlem43  46790  fourierdlem49  46795  fourierdlem73  46819  fourierdlem78  46824  fourierdlem103  46849  sqwvfourb  46869  etransclem46  46920  etransclem47  46921  sigarac  47492  sigaras  47495  sigarms  47496  sigariz  47503  sigarcol  47504  sharhght  47505  sigaradd  47506  nthrucw  47528  ceildivmod  48005  difmodm1lt  48025  2pwp1prm  48264  oexpnegALTV  48365  oexpnegnz  48366  itschlc0yqe  49459  itsclc0yqsol  49463  itsclquadb  49475  itscnhlinecirc02plem2  49482  amgmwlem  50510