Theorem negeqd 11372

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

Syntax hints:   → wi 4   = wceq 1541  -cneg 11363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-neg 11365

This theorem is referenced by:  negdi  11436  mulneg2  11572  mulm1  11576  ltord2  11664  leord2  11665  eqord2  11666  divneg  11831  div2neg  11862  recgt0  11985  infrenegsup  12123  supminf  12846  mul2lt0rlt0  13007  ceilval  13756  dfceil2  13757  ceilid  13769  modcyc2  13825  monoord2  13954  expval  13984  discr  14161  reneg  15046  imneg  15054  cjcj  15061  cjneg  15068  sqeqd  15087  telfsumo2  15724  infcvgaux1i  15778  infcvgaux2i  15779  risefallfac  15945  bpoly3  15979  sinneg  16069  tanneg  16071  sincossq  16099  odd2np1  16266  oexpneg  16270  modgcd  16457  pcneg  16800  mulgval  18999  mulgneg  19020  psgnunilem2  19422  evth2  24913  ivth2  25410  mbfposb  25608  mbfinf  25620  mbfi1flimlem  25677  iblcnlem  25744  iblrelem  25746  itgrevallem1  25750  iblneg  25758  itgneg  25759  ibladd  25776  ditgeq1  25803  ditgeq2  25804  ditgeq3  25805  ditgneg  25812  ditgswap  25814  dvrec  25913  dvrecg  25931  dvmptdiv  25932  dvexp3  25936  dvsincos  25939  rolle  25948  dvivth  25969  dvfsumge  25982  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsum2  25995  ftc2ditg  26007  vieta1lem2  26273  vieta1  26274  aaliou3lem2  26305  aaliou3lem8  26307  aaliou3lem5  26309  aaliou3lem6  26310  aaliou3lem7  26311  aaliou3  26313  sinperlem  26443  efimpi  26454  ptolemy  26459  sineq0  26487  efeq1  26491  tanregt0  26502  efif1olem2  26506  lognegb  26553  logneg2  26578  advlogexp  26618  logtayl  26623  logtayl2  26625  logccv  26626  cxpmul2z  26654  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  26954  emcllem7  26966  lgamgulmlem2  26994  ftalem5  27041  basellem5  27049  basellem9  27053  lgsneg1  27287  lgseisenlem1  27340  lgseisenlem4  27343  m1lgs  27353  2sqblem  27396  dchrisum0flblem1  27473  rpvmasum2  27477  pntrsumo1  27530  pntrlog2bndlem2  27543  pntibndlem2  27556  padicfval  27581  padicval  27582  ostth3  27603  brbtwn2  28927  colinearalglem4  28931  axsegconlem9  28947  ex-ceil  30472  nvabs  30696  ipasslem2  30856  sgnval2  32763  re0cj  32772  argcj  32777  numdenneg  32844  archirngz  33220  elrgspnlem1  33273  ccfldextdgrr  33778  constrrtcc  33841  constrnegcl  33869  constrrecl  33875  cos9thpiminplylem1  33888  cos9thpiminplylem2  33889  xrge0iifcv  34040  xrge0iifhom  34043  xrge0iif1  34044  xrge0tmd  34051  xrge0tmdALT  34052  fdvneggt  34706  fdvnegge  34708  climlec3  35877  ditgeq123dv  36364  cbvditgdavw  36425  cbvditgdavw2  36441  dvtan  37810  itg2addnclem3  37813  ibladdnc  37817  ftc1anclem5  37837  ftc1anclem6  37838  areacirclem1  37848  areacirc  37853  dffltz  42819  3cubeslem3r  42871  pellexlem6  43018  pell1234qrdich  43045  rmxm1  43118  rmym1  43119  monotoddzzfi  43126  monotoddzz  43127  oddcomabszz  43128  acongeq12d  43163  acongeq  43167  sineq0ALT  45119  infnsuprnmpt  45436  supminfrnmpt  45631  supminfxr  45650  neglimc  45833  dvcosax  46112  itgsin0pilem1  46136  itgsinexplem1  46140  itgsincmulx  46160  stoweidlem13  46199  stirlinglem5  46264  dirkerper  46282  dirkertrigeqlem3  46286  fourierdlem39  46332  fourierdlem40  46333  fourierdlem41  46334  fourierdlem43  46336  fourierdlem49  46341  fourierdlem73  46365  fourierdlem78  46370  fourierdlem103  46395  sqwvfourb  46415  etransclem46  46466  etransclem47  46467  sigarac  47038  sigaras  47041  sigarms  47042  sigariz  47049  sigarcol  47050  sharhght  47051  sigaradd  47052  nthrucw  47072  ceildivmod  47527  difmodm1lt  47547  2pwp1prm  47777  oexpnegALTV  47865  oexpnegnz  47866  itschlc0yqe  48948  itsclc0yqsol  48952  itsclquadb  48964  itscnhlinecirc02plem2  48971  amgmwlem  49989