Theorem negeqd 11389

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6456  df-fv 6508  df-ov 7372  df-neg 11382

This theorem is referenced by:  negdi  11453  mulneg2  11589  mulm1  11593  ltord2  11681  leord2  11682  eqord2  11683  divneg  11848  div2neg  11880  recgt0  12003  infrenegsup  12141  supminf  12887  mul2lt0rlt0  13048  ceilval  13799  dfceil2  13800  ceilid  13812  modcyc2  13868  monoord2  13997  expval  14027  discr  14204  reneg  15089  imneg  15097  cjcj  15104  cjneg  15111  sqeqd  15130  telfsumo2  15768  infcvgaux1i  15824  infcvgaux2i  15825  risefallfac  15991  bpoly3  16025  sinneg  16115  tanneg  16117  sincossq  16145  odd2np1  16312  oexpneg  16316  modgcd  16503  pcneg  16847  mulgval  19049  mulgneg  19070  psgnunilem2  19472  evth2  24929  ivth2  25424  mbfposb  25622  mbfinf  25634  mbfi1flimlem  25691  iblcnlem  25758  iblrelem  25760  itgrevallem1  25764  iblneg  25772  itgneg  25773  ibladd  25790  ditgeq1  25817  ditgeq2  25818  ditgeq3  25819  ditgneg  25826  ditgswap  25828  dvrec  25924  dvrecg  25942  dvmptdiv  25943  dvexp3  25947  dvsincos  25950  rolle  25959  dvivth  25979  dvfsumge  25991  dvfsumlem2  25996  dvfsum2  26003  ftc2ditg  26015  vieta1lem2  26279  vieta1  26280  aaliou3lem2  26311  aaliou3lem8  26313  aaliou3lem5  26315  aaliou3lem6  26316  aaliou3lem7  26317  aaliou3  26319  sinperlem  26446  efimpi  26457  ptolemy  26462  sineq0  26490  efeq1  26494  tanregt0  26505  efif1olem2  26509  lognegb  26556  logneg2  26581  advlogexp  26621  logtayl  26626  logtayl2  26628  logccv  26629  cxpmul2z  26657  logbrec  26748  cosangneg2d  26773  isosctrlem2  26785  isosctrlem3  26786  angpined  26796  dcubic1lem  26809  dcubic2  26810  mcubic  26813  cubic2  26814  dquart  26819  quart1lem  26821  quartlem1  26823  quart  26827  asinlem3a  26836  asinneg  26852  atanneg  26873  atancj  26876  atanlogaddlem  26879  atanlogsublem  26881  atantan  26889  atantayl  26903  birthdaylem3  26919  amgmlem  26955  emcllem7  26967  lgamgulmlem2  26995  ftalem5  27042  basellem5  27050  basellem9  27054  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  28976  colinearalglem4  28980  axsegconlem9  28996  ex-ceil  30520  nvabs  30745  ipasslem2  30905  sgnval2  32810  re0cj  32818  argcj  32823  numdenneg  32890  archirngz  33252  elrgspnlem1  33305  ccfldextdgrr  33818  constrrtcc  33881  constrnegcl  33909  constrrecl  33915  cos9thpiminplylem1  33928  cos9thpiminplylem2  33929  xrge0iifcv  34080  xrge0iifhom  34083  xrge0iif1  34084  xrge0tmd  34091  xrge0tmdALT  34092  fdvneggt  34746  fdvnegge  34748  climlec3  35918  ditgeq123dv  36405  cbvditgdavw  36466  cbvditgdavw2  36482  dvtan  37993  itg2addnclem3  37996  ibladdnc  38000  ftc1anclem5  38020  ftc1anclem6  38021  areacirclem1  38031  areacirc  38036  dffltz  43069  3cubeslem3r  43121  pellexlem6  43264  pell1234qrdich  43291  rmxm1  43364  rmym1  43365  monotoddzzfi  43372  monotoddzz  43373  oddcomabszz  43374  acongeq12d  43409  acongeq  43413  sineq0ALT  45365  infnsuprnmpt  45681  supminfrnmpt  45875  supminfxr  45894  neglimc  46077  dvcosax  46356  itgsin0pilem1  46380  itgsinexplem1  46384  itgsincmulx  46404  stoweidlem13  46443  stirlinglem5  46508  dirkerper  46526  dirkertrigeqlem3  46530  fourierdlem39  46576  fourierdlem40  46577  fourierdlem41  46578  fourierdlem43  46580  fourierdlem49  46585  fourierdlem73  46609  fourierdlem78  46614  fourierdlem103  46639  sqwvfourb  46659  etransclem46  46710  etransclem47  46711  sigarac  47282  sigaras  47285  sigarms  47286  sigariz  47293  sigarcol  47294  sharhght  47295  sigaradd  47296  nthrucw  47318  ceildivmod  47795  difmodm1lt  47815  2pwp1prm  48054  oexpnegALTV  48155  oexpnegnz  48156  itschlc0yqe  49238  itsclc0yqsol  49242  itsclquadb  49254  itscnhlinecirc02plem2  49261  amgmwlem  50279