Theorem negeqd 10880

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

Syntax hints:   → wi 4   = wceq 1537  -cneg 10871

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-neg 10873

This theorem is referenced by:  negdi  10943  mulneg2  11077  mulm1  11081  ltord2  11169  leord2  11170  eqord2  11171  divneg  11332  div2neg  11363  recgt0  11486  infrenegsup  11624  supminf  12336  mul2lt0rlt0  12492  ceilval  13209  dfceil2  13210  ceilid  13220  modcyc2  13276  monoord2  13402  expval  13432  discr  13602  reneg  14484  imneg  14492  cjcj  14499  cjneg  14506  sqeqd  14525  telfsumo2  15158  infcvgaux1i  15212  infcvgaux2i  15213  risefallfac  15378  bpoly3  15412  sinneg  15499  tanneg  15501  sincossq  15529  odd2np1  15690  oexpneg  15694  modgcd  15880  pcneg  16210  mulgval  18228  mulgneg  18246  psgnunilem2  18623  evth2  23564  ivth2  24056  mbfposb  24254  mbfinf  24266  mbfi1flimlem  24323  iblcnlem  24389  iblrelem  24391  itgrevallem1  24395  iblneg  24403  itgneg  24404  ibladd  24421  ditgeq1  24446  ditgeq2  24447  ditgeq3  24448  ditgneg  24455  ditgswap  24457  dvrec  24552  dvrecg  24570  dvmptdiv  24571  dvexp3  24575  dvsincos  24578  rolle  24587  dvivth  24607  dvfsumge  24619  dvfsumlem2  24624  dvfsum2  24631  ftc2ditg  24643  vieta1lem2  24900  vieta1  24901  aaliou3lem2  24932  aaliou3lem8  24934  aaliou3lem5  24936  aaliou3lem6  24937  aaliou3lem7  24938  aaliou3  24940  sinperlem  25066  efimpi  25077  ptolemy  25082  sineq0  25109  efeq1  25113  tanregt0  25123  efif1olem2  25127  lognegb  25173  logneg2  25198  advlogexp  25238  logtayl  25243  logtayl2  25245  logccv  25246  cxpmul2z  25274  logbrec  25360  cosangneg2d  25385  isosctrlem2  25397  isosctrlem3  25398  angpined  25408  dcubic1lem  25421  dcubic2  25422  mcubic  25425  cubic2  25426  dquart  25431  quart1lem  25433  quartlem1  25435  quart  25439  asinlem3a  25448  asinneg  25464  atanneg  25485  atancj  25488  atanlogaddlem  25491  atanlogsublem  25493  atantan  25501  atantayl  25515  birthdaylem3  25531  amgmlem  25567  emcllem7  25579  lgamgulmlem2  25607  ftalem5  25654  basellem5  25662  basellem9  25666  lgsneg1  25898  lgseisenlem1  25951  lgseisenlem4  25954  m1lgs  25964  2sqblem  26007  dchrisum0flblem1  26084  rpvmasum2  26088  pntrsumo1  26141  pntrlog2bndlem2  26154  pntibndlem2  26167  padicfval  26192  padicval  26193  ostth3  26214  brbtwn2  26691  colinearalglem4  26695  axsegconlem9  26711  ex-ceil  28227  nvabs  28449  ipasslem2  28609  numdenneg  30533  archirngz  30818  ccfldextdgrr  31057  xrge0iifcv  31177  xrge0iifhom  31180  xrge0iif1  31181  xrge0tmd  31188  xrge0tmdALT  31189  fdvneggt  31871  fdvnegge  31873  climlec3  32965  dvtan  34957  itg2addnclem3  34960  ibladdnc  34964  ftc1anclem5  34986  ftc1anclem6  34987  areacirclem1  34997  areacirc  35002  dffltz  39291  3cubeslem3r  39304  pellexlem6  39451  pell1234qrdich  39478  rmxm1  39551  rmym1  39552  monotoddzzfi  39559  monotoddzz  39560  oddcomabszz  39561  acongeq12d  39596  acongeq  39600  sineq0ALT  41291  infnsuprnmpt  41542  supminfrnmpt  41739  supminfxr  41760  neglimc  41948  dvcosax  42231  itgsin0pilem1  42255  itgsinexplem1  42259  itgsincmulx  42279  stoweidlem13  42318  stirlinglem5  42383  dirkerper  42401  dirkertrigeqlem3  42405  fourierdlem39  42451  fourierdlem40  42452  fourierdlem41  42453  fourierdlem43  42455  fourierdlem49  42460  fourierdlem73  42484  fourierdlem78  42489  fourierdlem103  42514  sqwvfourb  42534  etransclem46  42585  etransclem47  42586  sigarac  43129  sigaras  43132  sigarms  43133  sigariz  43140  sigarcol  43141  sharhght  43142  sigaradd  43143  2pwp1prm  43771  oexpnegALTV  43862  oexpnegnz  43863  itschlc0yqe  44767  itsclc0yqsol  44771  itsclquadb  44783  itscnhlinecirc02plem2  44790  amgmwlem  44923