Theorem negeqd 11454

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

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

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447

This theorem is referenced by:  negdi  11517  mulneg2  11651  mulm1  11655  ltord2  11743  leord2  11744  eqord2  11745  divneg  11906  div2neg  11937  recgt0  12060  infrenegsup  12197  supminf  12919  mul2lt0rlt0  13076  ceilval  13803  dfceil2  13804  ceilid  13816  modcyc2  13872  monoord2  13999  expval  14029  discr  14203  reneg  15072  imneg  15080  cjcj  15087  cjneg  15094  sqeqd  15113  telfsumo2  15749  infcvgaux1i  15803  infcvgaux2i  15804  risefallfac  15968  bpoly3  16002  sinneg  16089  tanneg  16091  sincossq  16119  odd2np1  16284  oexpneg  16288  modgcd  16474  pcneg  16807  mulgval  18954  mulgneg  18972  psgnunilem2  19363  evth2  24476  ivth2  24972  mbfposb  25170  mbfinf  25182  mbfi1flimlem  25240  iblcnlem  25306  iblrelem  25308  itgrevallem1  25312  iblneg  25320  itgneg  25321  ibladd  25338  ditgeq1  25365  ditgeq2  25366  ditgeq3  25367  ditgneg  25374  ditgswap  25376  dvrec  25472  dvrecg  25490  dvmptdiv  25491  dvexp3  25495  dvsincos  25498  rolle  25507  dvivth  25527  dvfsumge  25539  dvfsumlem2  25544  dvfsum2  25551  ftc2ditg  25563  vieta1lem2  25824  vieta1  25825  aaliou3lem2  25856  aaliou3lem8  25858  aaliou3lem5  25860  aaliou3lem6  25861  aaliou3lem7  25862  aaliou3  25864  sinperlem  25990  efimpi  26001  ptolemy  26006  sineq0  26033  efeq1  26037  tanregt0  26048  efif1olem2  26052  lognegb  26098  logneg2  26123  advlogexp  26163  logtayl  26168  logtayl2  26170  logccv  26171  cxpmul2z  26199  logbrec  26287  cosangneg2d  26312  isosctrlem2  26324  isosctrlem3  26325  angpined  26335  dcubic1lem  26348  dcubic2  26349  mcubic  26352  cubic2  26353  dquart  26358  quart1lem  26360  quartlem1  26362  quart  26366  asinlem3a  26375  asinneg  26391  atanneg  26412  atancj  26415  atanlogaddlem  26418  atanlogsublem  26420  atantan  26428  atantayl  26442  birthdaylem3  26458  amgmlem  26494  emcllem7  26506  lgamgulmlem2  26534  ftalem5  26581  basellem5  26589  basellem9  26593  lgsneg1  26825  lgseisenlem1  26878  lgseisenlem4  26881  m1lgs  26891  2sqblem  26934  dchrisum0flblem1  27011  rpvmasum2  27015  pntrsumo1  27068  pntrlog2bndlem2  27081  pntibndlem2  27094  padicfval  27119  padicval  27120  ostth3  27141  brbtwn2  28194  colinearalglem4  28198  axsegconlem9  28214  ex-ceil  29732  nvabs  29956  ipasslem2  30116  numdenneg  32054  archirngz  32366  ccfldextdgrr  32777  xrge0iifcv  32945  xrge0iifhom  32948  xrge0iif1  32949  xrge0tmd  32956  xrge0tmdALT  32957  fdvneggt  33643  fdvnegge  33645  climlec3  34734  gg-dvfsumlem2  35214  dvtan  36586  itg2addnclem3  36589  ibladdnc  36593  ftc1anclem5  36613  ftc1anclem6  36614  areacirclem1  36624  areacirc  36629  dffltz  41424  3cubeslem3r  41473  pellexlem6  41620  pell1234qrdich  41647  rmxm1  41721  rmym1  41722  monotoddzzfi  41729  monotoddzz  41730  oddcomabszz  41731  acongeq12d  41766  acongeq  41770  sineq0ALT  43746  infnsuprnmpt  44002  supminfrnmpt  44203  supminfxr  44222  neglimc  44411  dvcosax  44690  itgsin0pilem1  44714  itgsinexplem1  44718  itgsincmulx  44738  stoweidlem13  44777  stirlinglem5  44842  dirkerper  44860  dirkertrigeqlem3  44864  fourierdlem39  44910  fourierdlem40  44911  fourierdlem41  44912  fourierdlem43  44914  fourierdlem49  44919  fourierdlem73  44943  fourierdlem78  44948  fourierdlem103  44973  sqwvfourb  44993  etransclem46  45044  etransclem47  45045  sigarac  45616  sigaras  45619  sigarms  45620  sigariz  45627  sigarcol  45628  sharhght  45629  sigaradd  45630  2pwp1prm  46305  oexpnegALTV  46393  oexpnegnz  46394  itschlc0yqe  47494  itsclc0yqsol  47498  itsclquadb  47510  itscnhlinecirc02plem2  47517  amgmwlem  47897