Theorem negeqd 11425

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

Syntax hints:   → wi 4   = wceq 1561  -cneg 11416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6478  df-fv 6530  df-ov 7400  df-neg 11418

This theorem is referenced by:  negdi  11489  mulneg2  11625  mulm1  11629  ltord2  11717  leord2  11718  eqord2  11719  divneg  11883  div2neg  11915  recgt0  12038  infrenegsup  12176  supminf  12937  mul2lt0rlt0  13098  ceilval  13849  dfceil2  13850  ceilid  13862  modcyc2  13918  monoord2  14047  expval  14077  discr  14254  reneg  15153  imneg  15161  cjcj  15168  cjneg  15175  sqeqd  15194  telfsumo2  15832  infcvgaux1i  15888  infcvgaux2i  15889  risefallfac  16055  bpoly3  16089  sinneg  16179  tanneg  16181  sincossq  16209  odd2np1  16376  oexpneg  16380  modgcd  16567  pcneg  16911  mulgval  19114  mulgneg  19135  psgnunilem2  19536  evth2  25023  ivth2  25518  mbfposb  25716  mbfinf  25728  mbfi1flimlem  25785  iblcnlem  25852  iblrelem  25854  itgrevallem1  25858  iblneg  25866  itgneg  25867  ibladd  25884  ditgeq1  25911  ditgeq2  25912  ditgeq3  25913  ditgneg  25920  ditgswap  25922  dvrec  26018  dvrecg  26036  dvmptdiv  26037  dvexp3  26041  dvsincos  26044  rolle  26053  dvivth  26073  dvfsumge  26085  dvfsumlem2  26090  dvfsum2  26097  ftc2ditg  26109  vieta1lem2  26376  vieta1  26377  aaliou3lem2  26408  aaliou3lem8  26410  aaliou3lem5  26412  aaliou3lem6  26413  aaliou3lem7  26414  aaliou3  26416  sinperlem  26546  efimpi  26557  ptolemy  26562  sineq0  26590  efeq1  26594  tanregt0  26605  efif1olem2  26609  lognegb  26656  logneg2  26681  advlogexp  26721  logtayl  26726  logtayl2  26728  logccv  26729  cxpmul2z  26757  logbrec  26848  cosangneg2d  26873  isosctrlem2  26885  isosctrlem3  26886  angpined  26896  dcubic1lem  26909  dcubic2  26910  mcubic  26913  cubic2  26914  dquart  26919  quart1lem  26921  quartlem1  26923  quart  26927  asinlem3a  26936  asinneg  26952  atanneg  26973  atancj  26976  atanlogaddlem  26979  atanlogsublem  26981  atantan  26989  atantayl  27003  birthdaylem3  27019  amgmlem  27055  emcllem7  27067  lgamgulmlem2  27095  ftalem5  27142  basellem5  27150  basellem9  27154  lgsneg1  27387  lgseisenlem1  27440  lgseisenlem4  27443  m1lgs  27453  2sqblem  27496  dchrisum0flblem1  27573  rpvmasum2  27577  pntrsumo1  27630  pntrlog2bndlem2  27643  pntibndlem2  27656  padicfval  27681  padicval  27682  ostth3  27703  brbtwn2  29107  colinearalglem4  29111  axsegconlem9  29127  ex-ceil  30651  nvabs  30876  ipasslem2  31036  sgnval2  32938  re0cj  32946  argcj  32951  numdenneg  33018  archirngz  33370  elrgspnlem1  33424  ccfldextdgrr  33970  constrrtcc  34033  constrnegcl  34061  constrrecl  34067  cos9thpiminplylem1  34080  cos9thpiminplylem2  34081  xrge0iifcv  34232  xrge0iifhom  34235  xrge0iif1  34236  xrge0tmd  34243  xrge0tmdALT  34244  fdvneggt  34895  fdvnegge  34897  climlec3  36085  ditgeq123dv  36582  cbvditgdavw  36643  cbvditgdavw2  36659  dvtan  38170  itg2addnclem3  38173  ibladdnc  38177  ftc1anclem5  38197  ftc1anclem6  38198  areacirclem1  38208  areacirc  38213  dffltz  43217  3cubeslem3r  43269  pellexlem6  43412  pell1234qrdich  43439  rmxm1  43512  rmym1  43513  monotoddzzfi  43520  monotoddzz  43521  oddcomabszz  43522  acongeq12d  43557  acongeq  43561  sineq0ALT  45513  infnsuprnmpt  45826  supminfrnmpt  46020  supminfxr  46039  neglimc  46222  dvcosax  46501  itgsin0pilem1  46525  itgsinexplem1  46529  itgsincmulx  46549  stoweidlem13  46588  stirlinglem5  46653  dirkerper  46671  dirkertrigeqlem3  46675  fourierdlem39  46721  fourierdlem40  46722  fourierdlem41  46723  fourierdlem43  46725  fourierdlem49  46730  fourierdlem73  46754  fourierdlem78  46759  fourierdlem103  46784  sqwvfourb  46804  etransclem46  46855  etransclem47  46856  sigarac  47427  sigaras  47430  sigarms  47431  sigariz  47438  sigarcol  47439  sharhght  47440  sigaradd  47441  nthrucw  47463  ceildivmod  47940  difmodm1lt  47960  2pwp1prm  48199  oexpnegALTV  48300  oexpnegnz  48301  itschlc0yqe  49383  itsclc0yqsol  49387  itsclquadb  49399  itscnhlinecirc02plem2  49406  amgmwlem  50424