Theorem negeqd 11386

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379

This theorem is referenced by:  negdi  11450  mulneg2  11586  mulm1  11590  ltord2  11678  leord2  11679  eqord2  11680  divneg  11845  div2neg  11876  recgt0  11999  infrenegsup  12137  supminf  12860  mul2lt0rlt0  13021  ceilval  13770  dfceil2  13771  ceilid  13783  modcyc2  13839  monoord2  13968  expval  13998  discr  14175  reneg  15060  imneg  15068  cjcj  15075  cjneg  15082  sqeqd  15101  telfsumo2  15738  infcvgaux1i  15792  infcvgaux2i  15793  risefallfac  15959  bpoly3  15993  sinneg  16083  tanneg  16085  sincossq  16113  odd2np1  16280  oexpneg  16284  modgcd  16471  pcneg  16814  mulgval  19016  mulgneg  19037  psgnunilem2  19439  evth2  24930  ivth2  25427  mbfposb  25625  mbfinf  25637  mbfi1flimlem  25694  iblcnlem  25761  iblrelem  25763  itgrevallem1  25767  iblneg  25775  itgneg  25776  ibladd  25793  ditgeq1  25820  ditgeq2  25821  ditgeq3  25822  ditgneg  25829  ditgswap  25831  dvrec  25930  dvrecg  25948  dvmptdiv  25949  dvexp3  25953  dvsincos  25956  rolle  25965  dvivth  25986  dvfsumge  25999  dvfsumlem2  26004  dvfsumlem2OLD  26005  dvfsum2  26012  ftc2ditg  26024  vieta1lem2  26290  vieta1  26291  aaliou3lem2  26322  aaliou3lem8  26324  aaliou3lem5  26326  aaliou3lem6  26327  aaliou3lem7  26328  aaliou3  26330  sinperlem  26460  efimpi  26471  ptolemy  26476  sineq0  26504  efeq1  26508  tanregt0  26519  efif1olem2  26523  lognegb  26570  logneg2  26595  advlogexp  26635  logtayl  26640  logtayl2  26642  logccv  26643  cxpmul2z  26671  logbrec  26763  cosangneg2d  26788  isosctrlem2  26800  isosctrlem3  26801  angpined  26811  dcubic1lem  26824  dcubic2  26825  mcubic  26828  cubic2  26829  dquart  26834  quart1lem  26836  quartlem1  26838  quart  26842  asinlem3a  26851  asinneg  26867  atanneg  26888  atancj  26891  atanlogaddlem  26894  atanlogsublem  26896  atantan  26904  atantayl  26918  birthdaylem3  26934  amgmlem  26971  emcllem7  26983  lgamgulmlem2  27011  ftalem5  27058  basellem5  27066  basellem9  27070  lgsneg1  27304  lgseisenlem1  27357  lgseisenlem4  27360  m1lgs  27370  2sqblem  27413  dchrisum0flblem1  27490  rpvmasum2  27494  pntrsumo1  27547  pntrlog2bndlem2  27560  pntibndlem2  27573  padicfval  27598  padicval  27599  ostth3  27620  brbtwn2  28994  colinearalglem4  28998  axsegconlem9  29014  ex-ceil  30539  nvabs  30764  ipasslem2  30924  sgnval2  32829  re0cj  32838  argcj  32843  numdenneg  32910  archirngz  33287  elrgspnlem1  33340  ccfldextdgrr  33854  constrrtcc  33917  constrnegcl  33945  constrrecl  33951  cos9thpiminplylem1  33964  cos9thpiminplylem2  33965  xrge0iifcv  34116  xrge0iifhom  34119  xrge0iif1  34120  xrge0tmd  34127  xrge0tmdALT  34128  fdvneggt  34782  fdvnegge  34784  climlec3  35954  ditgeq123dv  36441  cbvditgdavw  36502  cbvditgdavw2  36518  dvtan  37925  itg2addnclem3  37928  ibladdnc  37932  ftc1anclem5  37952  ftc1anclem6  37953  areacirclem1  37963  areacirc  37968  dffltz  42996  3cubeslem3r  43048  pellexlem6  43195  pell1234qrdich  43222  rmxm1  43295  rmym1  43296  monotoddzzfi  43303  monotoddzz  43304  oddcomabszz  43305  acongeq12d  43340  acongeq  43344  sineq0ALT  45296  infnsuprnmpt  45612  supminfrnmpt  45807  supminfxr  45826  neglimc  46009  dvcosax  46288  itgsin0pilem1  46312  itgsinexplem1  46316  itgsincmulx  46336  stoweidlem13  46375  stirlinglem5  46440  dirkerper  46458  dirkertrigeqlem3  46462  fourierdlem39  46508  fourierdlem40  46509  fourierdlem41  46510  fourierdlem43  46512  fourierdlem49  46517  fourierdlem73  46541  fourierdlem78  46546  fourierdlem103  46571  sqwvfourb  46591  etransclem46  46642  etransclem47  46643  sigarac  47214  sigaras  47217  sigarms  47218  sigariz  47225  sigarcol  47226  sharhght  47227  sigaradd  47228  nthrucw  47248  ceildivmod  47703  difmodm1lt  47723  2pwp1prm  47953  oexpnegALTV  48041  oexpnegnz  48042  itschlc0yqe  49124  itsclc0yqsol  49128  itsclquadb  49140  itscnhlinecirc02plem2  49147  amgmwlem  50165