Theorem negeqd 11484

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-ov 7416  df-neg 11477

This theorem is referenced by:  negdi  11548  mulneg2  11682  mulm1  11686  ltord2  11774  leord2  11775  eqord2  11776  divneg  11941  div2neg  11972  recgt0  12095  infrenegsup  12233  supminf  12959  mul2lt0rlt0  13119  ceilval  13860  dfceil2  13861  ceilid  13873  modcyc2  13929  monoord2  14056  expval  14086  discr  14261  reneg  15146  imneg  15154  cjcj  15161  cjneg  15168  sqeqd  15187  telfsumo2  15821  infcvgaux1i  15875  infcvgaux2i  15876  risefallfac  16042  bpoly3  16076  sinneg  16164  tanneg  16166  sincossq  16194  odd2np1  16360  oexpneg  16364  modgcd  16551  pcneg  16894  mulgval  19058  mulgneg  19079  psgnunilem2  19481  evth2  24928  ivth2  25426  mbfposb  25624  mbfinf  25636  mbfi1flimlem  25693  iblcnlem  25760  iblrelem  25762  itgrevallem1  25766  iblneg  25774  itgneg  25775  ibladd  25792  ditgeq1  25819  ditgeq2  25820  ditgeq3  25821  ditgneg  25828  ditgswap  25830  dvrec  25929  dvrecg  25947  dvmptdiv  25948  dvexp3  25952  dvsincos  25955  rolle  25964  dvivth  25985  dvfsumge  25998  dvfsumlem2  26003  dvfsumlem2OLD  26004  dvfsum2  26011  ftc2ditg  26023  vieta1lem2  26289  vieta1  26290  aaliou3lem2  26321  aaliou3lem8  26323  aaliou3lem5  26325  aaliou3lem6  26326  aaliou3lem7  26327  aaliou3  26329  sinperlem  26458  efimpi  26469  ptolemy  26474  sineq0  26502  efeq1  26506  tanregt0  26517  efif1olem2  26521  lognegb  26568  logneg2  26593  advlogexp  26633  logtayl  26638  logtayl2  26640  logccv  26641  cxpmul2z  26669  logbrec  26761  cosangneg2d  26786  isosctrlem2  26798  isosctrlem3  26799  angpined  26809  dcubic1lem  26822  dcubic2  26823  mcubic  26826  cubic2  26827  dquart  26832  quart1lem  26834  quartlem1  26836  quart  26840  asinlem3a  26849  asinneg  26865  atanneg  26886  atancj  26889  atanlogaddlem  26892  atanlogsublem  26894  atantan  26902  atantayl  26916  birthdaylem3  26932  amgmlem  26969  emcllem7  26981  lgamgulmlem2  27009  ftalem5  27056  basellem5  27064  basellem9  27068  lgsneg1  27302  lgseisenlem1  27355  lgseisenlem4  27358  m1lgs  27368  2sqblem  27411  dchrisum0flblem1  27488  rpvmasum2  27492  pntrsumo1  27545  pntrlog2bndlem2  27558  pntibndlem2  27571  padicfval  27596  padicval  27597  ostth3  27618  brbtwn2  28850  colinearalglem4  28854  axsegconlem9  28870  ex-ceil  30395  nvabs  30619  ipasslem2  30779  re0cj  32688  numdenneg  32756  archirngz  33135  elrgspnlem1  33185  ccfldextdgrr  33659  constrrtcc  33715  constrnegcl  33743  xrge0iifcv  33892  xrge0iifhom  33895  xrge0iif1  33896  xrge0tmd  33903  xrge0tmdALT  33904  fdvneggt  34574  fdvnegge  34576  climlec3  35693  ditgeq123dv  36181  cbvditgdavw  36242  cbvditgdavw2  36258  dvtan  37636  itg2addnclem3  37639  ibladdnc  37643  ftc1anclem5  37663  ftc1anclem6  37664  areacirclem1  37674  areacirc  37679  dffltz  42607  3cubeslem3r  42661  pellexlem6  42808  pell1234qrdich  42835  rmxm1  42909  rmym1  42910  monotoddzzfi  42917  monotoddzz  42918  oddcomabszz  42919  acongeq12d  42954  acongeq  42958  sineq0ALT  44914  infnsuprnmpt  45214  supminfrnmpt  45413  supminfxr  45432  neglimc  45619  dvcosax  45898  itgsin0pilem1  45922  itgsinexplem1  45926  itgsincmulx  45946  stoweidlem13  45985  stirlinglem5  46050  dirkerper  46068  dirkertrigeqlem3  46072  fourierdlem39  46118  fourierdlem40  46119  fourierdlem41  46120  fourierdlem43  46122  fourierdlem49  46127  fourierdlem73  46151  fourierdlem78  46156  fourierdlem103  46181  sqwvfourb  46201  etransclem46  46252  etransclem47  46253  sigarac  46824  sigaras  46827  sigarms  46828  sigariz  46835  sigarcol  46836  sharhght  46837  sigaradd  46838  ceildivmod  47299  2pwp1prm  47534  oexpnegALTV  47622  oexpnegnz  47623  itschlc0yqe  48639  itsclc0yqsol  48643  itsclquadb  48655  itscnhlinecirc02plem2  48662  amgmwlem  49329