Theorem negeqd 10911

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

Syntax hints:   → wi 4   = wceq 1539  -cneg 10902

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-un 3864  df-in 3866  df-ss 3876  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-iota 6295  df-fv 6344  df-ov 7154  df-neg 10904

This theorem is referenced by:  negdi  10974  mulneg2  11108  mulm1  11112  ltord2  11200  leord2  11201  eqord2  11202  divneg  11363  div2neg  11394  recgt0  11517  infrenegsup  11653  supminf  12368  mul2lt0rlt0  12525  ceilval  13250  dfceil2  13251  ceilid  13261  modcyc2  13317  monoord2  13444  expval  13474  discr  13644  reneg  14525  imneg  14533  cjcj  14540  cjneg  14547  sqeqd  14566  telfsumo2  15199  infcvgaux1i  15253  infcvgaux2i  15254  risefallfac  15419  bpoly3  15453  sinneg  15540  tanneg  15542  sincossq  15570  odd2np1  15735  oexpneg  15739  modgcd  15924  pcneg  16258  mulgval  18288  mulgneg  18306  psgnunilem2  18683  evth2  23654  ivth2  24148  mbfposb  24346  mbfinf  24358  mbfi1flimlem  24415  iblcnlem  24481  iblrelem  24483  itgrevallem1  24487  iblneg  24495  itgneg  24496  ibladd  24513  ditgeq1  24540  ditgeq2  24541  ditgeq3  24542  ditgneg  24549  ditgswap  24551  dvrec  24647  dvrecg  24665  dvmptdiv  24666  dvexp3  24670  dvsincos  24673  rolle  24682  dvivth  24702  dvfsumge  24714  dvfsumlem2  24719  dvfsum2  24726  ftc2ditg  24738  vieta1lem2  24999  vieta1  25000  aaliou3lem2  25031  aaliou3lem8  25033  aaliou3lem5  25035  aaliou3lem6  25036  aaliou3lem7  25037  aaliou3  25039  sinperlem  25165  efimpi  25176  ptolemy  25181  sineq0  25208  efeq1  25212  tanregt0  25223  efif1olem2  25227  lognegb  25273  logneg2  25298  advlogexp  25338  logtayl  25343  logtayl2  25345  logccv  25346  cxpmul2z  25374  logbrec  25460  cosangneg2d  25485  isosctrlem2  25497  isosctrlem3  25498  angpined  25508  dcubic1lem  25521  dcubic2  25522  mcubic  25525  cubic2  25526  dquart  25531  quart1lem  25533  quartlem1  25535  quart  25539  asinlem3a  25548  asinneg  25564  atanneg  25585  atancj  25588  atanlogaddlem  25591  atanlogsublem  25593  atantan  25601  atantayl  25615  birthdaylem3  25631  amgmlem  25667  emcllem7  25679  lgamgulmlem2  25707  ftalem5  25754  basellem5  25762  basellem9  25766  lgsneg1  25998  lgseisenlem1  26051  lgseisenlem4  26054  m1lgs  26064  2sqblem  26107  dchrisum0flblem1  26184  rpvmasum2  26188  pntrsumo1  26241  pntrlog2bndlem2  26254  pntibndlem2  26267  padicfval  26292  padicval  26293  ostth3  26314  brbtwn2  26791  colinearalglem4  26795  axsegconlem9  26811  ex-ceil  28325  nvabs  28547  ipasslem2  28707  numdenneg  30648  archirngz  30962  ccfldextdgrr  31256  xrge0iifcv  31398  xrge0iifhom  31401  xrge0iif1  31402  xrge0tmd  31409  xrge0tmdALT  31410  fdvneggt  32092  fdvnegge  32094  climlec3  33207  dvtan  35380  itg2addnclem3  35383  ibladdnc  35387  ftc1anclem5  35407  ftc1anclem6  35408  areacirclem1  35418  areacirc  35423  dffltz  39956  3cubeslem3r  39994  pellexlem6  40141  pell1234qrdich  40168  rmxm1  40241  rmym1  40242  monotoddzzfi  40249  monotoddzz  40250  oddcomabszz  40251  acongeq12d  40286  acongeq  40290  sineq0ALT  42009  infnsuprnmpt  42249  supminfrnmpt  42441  supminfxr  42462  neglimc  42648  dvcosax  42927  itgsin0pilem1  42951  itgsinexplem1  42955  itgsincmulx  42975  stoweidlem13  43014  stirlinglem5  43079  dirkerper  43097  dirkertrigeqlem3  43101  fourierdlem39  43147  fourierdlem40  43148  fourierdlem41  43149  fourierdlem43  43151  fourierdlem49  43156  fourierdlem73  43180  fourierdlem78  43185  fourierdlem103  43210  sqwvfourb  43230  etransclem46  43281  etransclem47  43282  sigarac  43825  sigaras  43828  sigarms  43829  sigariz  43836  sigarcol  43837  sharhght  43838  sigaradd  43839  2pwp1prm  44467  oexpnegALTV  44555  oexpnegnz  44556  itschlc0yqe  45532  itsclc0yqsol  45536  itsclquadb  45548  itscnhlinecirc02plem2  45555  amgmwlem  45714