Theorem negeqd 11224

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

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

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-neg 11217

This theorem is referenced by:  negdi  11287  mulneg2  11421  mulm1  11425  ltord2  11513  leord2  11514  eqord2  11515  divneg  11676  div2neg  11707  recgt0  11830  infrenegsup  11967  supminf  12684  mul2lt0rlt0  12841  ceilval  13567  dfceil2  13568  ceilid  13580  modcyc2  13636  monoord2  13763  expval  13793  discr  13964  reneg  14845  imneg  14853  cjcj  14860  cjneg  14867  sqeqd  14886  telfsumo2  15524  infcvgaux1i  15578  infcvgaux2i  15579  risefallfac  15743  bpoly3  15777  sinneg  15864  tanneg  15866  sincossq  15894  odd2np1  16059  oexpneg  16063  modgcd  16249  pcneg  16584  mulgval  18713  mulgneg  18731  psgnunilem2  19112  evth2  24132  ivth2  24628  mbfposb  24826  mbfinf  24838  mbfi1flimlem  24896  iblcnlem  24962  iblrelem  24964  itgrevallem1  24968  iblneg  24976  itgneg  24977  ibladd  24994  ditgeq1  25021  ditgeq2  25022  ditgeq3  25023  ditgneg  25030  ditgswap  25032  dvrec  25128  dvrecg  25146  dvmptdiv  25147  dvexp3  25151  dvsincos  25154  rolle  25163  dvivth  25183  dvfsumge  25195  dvfsumlem2  25200  dvfsum2  25207  ftc2ditg  25219  vieta1lem2  25480  vieta1  25481  aaliou3lem2  25512  aaliou3lem8  25514  aaliou3lem5  25516  aaliou3lem6  25517  aaliou3lem7  25518  aaliou3  25520  sinperlem  25646  efimpi  25657  ptolemy  25662  sineq0  25689  efeq1  25693  tanregt0  25704  efif1olem2  25708  lognegb  25754  logneg2  25779  advlogexp  25819  logtayl  25824  logtayl2  25826  logccv  25827  cxpmul2z  25855  logbrec  25941  cosangneg2d  25966  isosctrlem2  25978  isosctrlem3  25979  angpined  25989  dcubic1lem  26002  dcubic2  26003  mcubic  26006  cubic2  26007  dquart  26012  quart1lem  26014  quartlem1  26016  quart  26020  asinlem3a  26029  asinneg  26045  atanneg  26066  atancj  26069  atanlogaddlem  26072  atanlogsublem  26074  atantan  26082  atantayl  26096  birthdaylem3  26112  amgmlem  26148  emcllem7  26160  lgamgulmlem2  26188  ftalem5  26235  basellem5  26243  basellem9  26247  lgsneg1  26479  lgseisenlem1  26532  lgseisenlem4  26535  m1lgs  26545  2sqblem  26588  dchrisum0flblem1  26665  rpvmasum2  26669  pntrsumo1  26722  pntrlog2bndlem2  26735  pntibndlem2  26748  padicfval  26773  padicval  26774  ostth3  26795  brbtwn2  27282  colinearalglem4  27286  axsegconlem9  27302  ex-ceil  28821  nvabs  29043  ipasslem2  29203  numdenneg  31140  archirngz  31452  ccfldextdgrr  31751  xrge0iifcv  31893  xrge0iifhom  31896  xrge0iif1  31897  xrge0tmd  31904  xrge0tmdALT  31905  fdvneggt  32589  fdvnegge  32591  climlec3  33708  dvtan  35836  itg2addnclem3  35839  ibladdnc  35843  ftc1anclem5  35863  ftc1anclem6  35864  areacirclem1  35874  areacirc  35879  dffltz  40478  3cubeslem3r  40516  pellexlem6  40663  pell1234qrdich  40690  rmxm1  40763  rmym1  40764  monotoddzzfi  40771  monotoddzz  40772  oddcomabszz  40773  acongeq12d  40808  acongeq  40812  sineq0ALT  42564  infnsuprnmpt  42803  supminfrnmpt  42992  supminfxr  43011  neglimc  43195  dvcosax  43474  itgsin0pilem1  43498  itgsinexplem1  43502  itgsincmulx  43522  stoweidlem13  43561  stirlinglem5  43626  dirkerper  43644  dirkertrigeqlem3  43648  fourierdlem39  43694  fourierdlem40  43695  fourierdlem41  43696  fourierdlem43  43698  fourierdlem49  43703  fourierdlem73  43727  fourierdlem78  43732  fourierdlem103  43757  sqwvfourb  43777  etransclem46  43828  etransclem47  43829  sigarac  44379  sigaras  44382  sigarms  44383  sigariz  44390  sigarcol  44391  sharhght  44392  sigaradd  44393  2pwp1prm  45052  oexpnegALTV  45140  oexpnegnz  45141  itschlc0yqe  46117  itsclc0yqsol  46121  itsclquadb  46133  itscnhlinecirc02plem2  46140  amgmwlem  46517