Theorem negeqd 11387

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380

This theorem is referenced by:  negdi  11451  mulneg2  11587  mulm1  11591  ltord2  11679  leord2  11680  eqord2  11681  divneg  11846  div2neg  11878  recgt0  12001  infrenegsup  12139  supminf  12885  mul2lt0rlt0  13046  ceilval  13797  dfceil2  13798  ceilid  13810  modcyc2  13866  monoord2  13995  expval  14025  discr  14202  reneg  15087  imneg  15095  cjcj  15102  cjneg  15109  sqeqd  15128  telfsumo2  15766  infcvgaux1i  15822  infcvgaux2i  15823  risefallfac  15989  bpoly3  16023  sinneg  16113  tanneg  16115  sincossq  16143  odd2np1  16310  oexpneg  16314  modgcd  16501  pcneg  16845  mulgval  19047  mulgneg  19068  psgnunilem2  19470  evth2  24927  ivth2  25422  mbfposb  25620  mbfinf  25632  mbfi1flimlem  25689  iblcnlem  25756  iblrelem  25758  itgrevallem1  25762  iblneg  25770  itgneg  25771  ibladd  25788  ditgeq1  25815  ditgeq2  25816  ditgeq3  25817  ditgneg  25824  ditgswap  25826  dvrec  25922  dvrecg  25940  dvmptdiv  25941  dvexp3  25945  dvsincos  25948  rolle  25957  dvivth  25977  dvfsumge  25989  dvfsumlem2  25994  dvfsum2  26001  ftc2ditg  26013  vieta1lem2  26277  vieta1  26278  aaliou3lem2  26309  aaliou3lem8  26311  aaliou3lem5  26313  aaliou3lem6  26314  aaliou3lem7  26315  aaliou3  26317  sinperlem  26444  efimpi  26455  ptolemy  26460  sineq0  26488  efeq1  26492  tanregt0  26503  efif1olem2  26507  lognegb  26554  logneg2  26579  advlogexp  26619  logtayl  26624  logtayl2  26626  logccv  26627  cxpmul2z  26655  logbrec  26746  cosangneg2d  26771  isosctrlem2  26783  isosctrlem3  26784  angpined  26794  dcubic1lem  26807  dcubic2  26808  mcubic  26811  cubic2  26812  dquart  26817  quart1lem  26819  quartlem1  26821  quart  26825  asinlem3a  26834  asinneg  26850  atanneg  26871  atancj  26874  atanlogaddlem  26877  atanlogsublem  26879  atantan  26887  atantayl  26901  birthdaylem3  26917  amgmlem  26953  emcllem7  26965  lgamgulmlem2  26993  ftalem5  27040  basellem5  27048  basellem9  27052  lgsneg1  27285  lgseisenlem1  27338  lgseisenlem4  27341  m1lgs  27351  2sqblem  27394  dchrisum0flblem1  27471  rpvmasum2  27475  pntrsumo1  27528  pntrlog2bndlem2  27541  pntibndlem2  27554  padicfval  27579  padicval  27580  ostth3  27601  brbtwn2  28974  colinearalglem4  28978  axsegconlem9  28994  ex-ceil  30518  nvabs  30743  ipasslem2  30903  sgnval2  32808  re0cj  32816  argcj  32821  numdenneg  32888  archirngz  33250  elrgspnlem1  33303  ccfldextdgrr  33816  constrrtcc  33879  constrnegcl  33907  constrrecl  33913  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  xrge0iifcv  34078  xrge0iifhom  34081  xrge0iif1  34082  xrge0tmd  34089  xrge0tmdALT  34090  fdvneggt  34744  fdvnegge  34746  climlec3  35916  ditgeq123dv  36403  cbvditgdavw  36464  cbvditgdavw2  36480  dvtan  37991  itg2addnclem3  37994  ibladdnc  37998  ftc1anclem5  38018  ftc1anclem6  38019  areacirclem1  38029  areacirc  38034  dffltz  43067  3cubeslem3r  43119  pellexlem6  43262  pell1234qrdich  43289  rmxm1  43362  rmym1  43363  monotoddzzfi  43370  monotoddzz  43371  oddcomabszz  43372  acongeq12d  43407  acongeq  43411  sineq0ALT  45363  infnsuprnmpt  45679  supminfrnmpt  45873  supminfxr  45892  neglimc  46075  dvcosax  46354  itgsin0pilem1  46378  itgsinexplem1  46382  itgsincmulx  46402  stoweidlem13  46441  stirlinglem5  46506  dirkerper  46524  dirkertrigeqlem3  46528  fourierdlem39  46574  fourierdlem40  46575  fourierdlem41  46576  fourierdlem43  46578  fourierdlem49  46583  fourierdlem73  46607  fourierdlem78  46612  fourierdlem103  46637  sqwvfourb  46657  etransclem46  46708  etransclem47  46709  sigarac  47280  sigaras  47283  sigarms  47284  sigariz  47291  sigarcol  47292  sharhght  47293  sigaradd  47294  nthrucw  47316  ceildivmod  47793  difmodm1lt  47813  2pwp1prm  48052  oexpnegALTV  48153  oexpnegnz  48154  itschlc0yqe  49236  itsclc0yqsol  49240  itsclquadb  49252  itscnhlinecirc02plem2  49259  amgmwlem  50277