Theorem negeqd 11551

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   -cneg 11542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11544

This theorem is used by:  negdi  11615  mulneg2  11753  mulm1  11757  ltord2  11845  leord2  11846  eqord2  11847  divneg  12008  div2neg  12040  recgt0  12163  infrenegsup  12300  supminf  13062  mul2lt0rlt0  13224  ceilval  13978  dfceil2  13979  ceilid  13991  modcyc2  14047  monoord2  14176  expval  14206  discr  14384  reneg  15292  imneg  15300  cjcj  15307  cjneg  15314  sqeqd  15333  telfsumo2  15970  infcvgaux1i  16026  infcvgaux2i  16027  risefallfac  16191  bpoly3  16224  sinneg  16314  tanneg  16316  sincossq  16344  odd2np1  16511  oexpneg  16515  modgcd  16705  pcneg  17052  mulgval  19281  mulgneg  19302  psgnunilem2  19709  evth2  25281  ivth2  25776  mbfposb  25974  mbfinf  25986  mbfi1flimlem  26043  iblcnlem  26109  iblrelem  26111  itgrevallem1  26115  iblneg  26123  itgneg  26124  ibladd  26141  ditgeq1  26168  ditgeq2  26169  ditgeq3  26170  ditgneg  26177  ditgswap  26179  dvrec  26275  dvrecg  26293  dvmptdiv  26294  dvexp3  26298  dvsincos  26301  rolle  26310  dvivth  26330  dvfsumge  26342  dvfsumlem2  26347  dvfsum2  26354  ftc2ditg  26366  vieta1lem2  26634  vieta1  26635  aaliou3lem2  26670  aaliou3lem8  26672  aaliou3lem5  26674  aaliou3lem6  26675  aaliou3lem7  26676  aaliou3  26678  aaliou3r  26679  sinperlem  26809  efimpi  26820  ptolemy  26825  sineq0  26852  efeq1  26856  tanregt0  26867  efif1olem2  26871  lognegb  26918  logneg2  26943  advlogexp  26983  logtayl  26988  logtayl2  26990  logccv  26991  cxpmul2z  27019  logbrec  27110  cosangneg2d  27135  isosctrlem2  27147  isosctrlem3  27148  angpined  27158  dcubic1lem  27171  dcubic2  27172  mcubic  27175  cubic2  27176  dquart  27181  quart1lem  27183  quartlem1  27185  quart  27189  asinlem3a  27198  asinneg  27214  atanneg  27235  atancj  27238  atanlogaddlem  27241  atanlogsublem  27243  atantan  27251  atantayl  27265  birthdaylem3  27281  amgmlem  27317  emcllem7  27329  lgamgulmlem2  27357  ftalem5  27404  basellem5  27412  basellem9  27416  lgsneg1  27649  lgseisenlem1  27702  lgseisenlem4  27705  m1lgs  27715  2sqblem  27758  dchrisum0flblem1  27835  rpvmasum2  27839  pntrsumo1  27892  pntrlog2bndlem2  27905  pntibndlem2  27918  padicfval  27943  padicval  27944  ostth3  27965  brbtwn2  29483  colinearalglem4  29487  axsegconlem9  29503  ex-ceil  31049  nvabs  31274  ipasslem2  31434  sgnval2  33327  re0cj  33335  argcj  33340  numdenneg  33406  archirngz  33750  elrgspnlem1  33803  ccfldextdgrr  34304  constrrtcc  34367  constrnegcl  34395  constrrecl  34401  cos9thpiminplylem1  34414  cos9thpiminplylem2  34415  xrge0iifcv  34566  xrge0iifhom  34569  xrge0iif1  34570  xrge0tmd  34577  xrge0tmdALT  34578  fdvneggt  35229  fdvnegge  35231  climlec3  36499  ditgeq123dv  37010  cbvditgdavw  37071  cbvditgdavw2  37087  dvtan  38588  itg2addnclem3  38591  ibladdnc  38595  ftc1anclem5  38615  ftc1anclem6  38616  areacirclem1  38626  areacirc  38631  25or6to4  43256  dffltz  43670  3cubeslem3r  43697  pellexlem6  43840  pell1234qrdich  43867  rmxm1  43940  rmym1  43941  monotoddzzfi  43948  monotoddzz  43949  oddcomabszz  43950  acongeq12d  43985  acongeq  43989  sineq0ALT  45918  infnsuprnmpt  46261  supminfrnmpt  46454  supminfxr  46473  neglimc  46656  dvcosax  46935  itgsin0pilem1  46959  itgsinexplem1  46963  itgsincmulx  46983  stoweidlem13  47022  stirlinglem5  47087  dirkerper  47105  dirkertrigeqlem3  47109  fourierdlem39  47155  fourierdlem40  47156  fourierdlem41  47157  fourierdlem43  47159  fourierdlem49  47164  fourierdlem73  47188  fourierdlem78  47193  fourierdlem103  47218  sqwvfourb  47238  etransclem46  47289  etransclem47  47290  sigarac  47861  sigaras  47864  sigarms  47865  sigariz  47872  sigarcol  47873  sharhght  47874  sigaradd  47875  ceildivmod  48414  difmodm1lt  48434  2pwp1prm  48673  oexpnegALTV  48774  oexpnegnz  48775  itschlc0yqe  49871  itsclc0yqsol  49875  itsclquadb  49887  itscnhlinecirc02plem2  49894  dvsec  50855  dvcsc  50856  dvcot  50857  crosspaltd  50965  amgmwlem  50986