Theorem negeqd 11424

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

Syntax hints:   → wi 4   = wceq 1560  -cneg 11415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-neg 11417

This theorem is referenced by:  negdi  11488  mulneg2  11624  mulm1  11628  ltord2  11716  leord2  11717  eqord2  11718  divneg  11882  div2neg  11914  recgt0  12037  infrenegsup  12175  supminf  12936  mul2lt0rlt0  13097  ceilval  13848  dfceil2  13849  ceilid  13861  modcyc2  13917  monoord2  14046  expval  14076  discr  14253  reneg  15152  imneg  15160  cjcj  15167  cjneg  15174  sqeqd  15193  telfsumo2  15831  infcvgaux1i  15887  infcvgaux2i  15888  risefallfac  16054  bpoly3  16088  sinneg  16178  tanneg  16180  sincossq  16208  odd2np1  16375  oexpneg  16379  modgcd  16566  pcneg  16910  mulgval  19113  mulgneg  19134  psgnunilem2  19535  evth2  25022  ivth2  25517  mbfposb  25715  mbfinf  25727  mbfi1flimlem  25784  iblcnlem  25851  iblrelem  25853  itgrevallem1  25857  iblneg  25865  itgneg  25866  ibladd  25883  ditgeq1  25910  ditgeq2  25911  ditgeq3  25912  ditgneg  25919  ditgswap  25921  dvrec  26017  dvrecg  26035  dvmptdiv  26036  dvexp3  26040  dvsincos  26043  rolle  26052  dvivth  26072  dvfsumge  26084  dvfsumlem2  26089  dvfsum2  26096  ftc2ditg  26108  vieta1lem2  26375  vieta1  26376  aaliou3lem2  26407  aaliou3lem8  26409  aaliou3lem5  26411  aaliou3lem6  26412  aaliou3lem7  26413  aaliou3  26415  sinperlem  26545  efimpi  26556  ptolemy  26561  sineq0  26589  efeq1  26593  tanregt0  26604  efif1olem2  26608  lognegb  26655  logneg2  26680  advlogexp  26720  logtayl  26725  logtayl2  26727  logccv  26728  cxpmul2z  26756  logbrec  26847  cosangneg2d  26872  isosctrlem2  26884  isosctrlem3  26885  angpined  26895  dcubic1lem  26908  dcubic2  26909  mcubic  26912  cubic2  26913  dquart  26918  quart1lem  26920  quartlem1  26922  quart  26926  asinlem3a  26935  asinneg  26951  atanneg  26972  atancj  26975  atanlogaddlem  26978  atanlogsublem  26980  atantan  26988  atantayl  27002  birthdaylem3  27018  amgmlem  27054  emcllem7  27066  lgamgulmlem2  27094  ftalem5  27141  basellem5  27149  basellem9  27153  lgsneg1  27386  lgseisenlem1  27439  lgseisenlem4  27442  m1lgs  27452  2sqblem  27495  dchrisum0flblem1  27572  rpvmasum2  27576  pntrsumo1  27629  pntrlog2bndlem2  27642  pntibndlem2  27655  padicfval  27680  padicval  27681  ostth3  27702  brbtwn2  29106  colinearalglem4  29110  axsegconlem9  29126  ex-ceil  30650  nvabs  30875  ipasslem2  31035  sgnval2  32937  re0cj  32945  argcj  32950  numdenneg  33017  archirngz  33369  elrgspnlem1  33423  ccfldextdgrr  33969  constrrtcc  34032  constrnegcl  34060  constrrecl  34066  cos9thpiminplylem1  34079  cos9thpiminplylem2  34080  xrge0iifcv  34231  xrge0iifhom  34234  xrge0iif1  34235  xrge0tmd  34242  xrge0tmdALT  34243  fdvneggt  34894  fdvnegge  34896  climlec3  36084  ditgeq123dv  36581  cbvditgdavw  36642  cbvditgdavw2  36658  dvtan  38169  itg2addnclem3  38172  ibladdnc  38176  ftc1anclem5  38196  ftc1anclem6  38197  areacirclem1  38207  areacirc  38212  dffltz  43216  3cubeslem3r  43268  pellexlem6  43411  pell1234qrdich  43438  rmxm1  43511  rmym1  43512  monotoddzzfi  43519  monotoddzz  43520  oddcomabszz  43521  acongeq12d  43556  acongeq  43560  sineq0ALT  45512  infnsuprnmpt  45825  supminfrnmpt  46019  supminfxr  46038  neglimc  46221  dvcosax  46500  itgsin0pilem1  46524  itgsinexplem1  46528  itgsincmulx  46548  stoweidlem13  46587  stirlinglem5  46652  dirkerper  46670  dirkertrigeqlem3  46674  fourierdlem39  46720  fourierdlem40  46721  fourierdlem41  46722  fourierdlem43  46724  fourierdlem49  46729  fourierdlem73  46753  fourierdlem78  46758  fourierdlem103  46783  sqwvfourb  46803  etransclem46  46854  etransclem47  46855  sigarac  47426  sigaras  47429  sigarms  47430  sigariz  47437  sigarcol  47438  sharhght  47439  sigaradd  47440  nthrucw  47462  ceildivmod  47939  difmodm1lt  47959  2pwp1prm  48198  oexpnegALTV  48299  oexpnegnz  48300  itschlc0yqe  49382  itsclc0yqsol  49386  itsclquadb  49398  itscnhlinecirc02plem2  49405  amgmwlem  50423