Theorem negeqd 11450

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

Syntax hints:   → wi 4   = wceq 1541  -cneg 11441

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-neg 11443

This theorem is referenced by:  negdi  11513  mulneg2  11647  mulm1  11651  ltord2  11739  leord2  11740  eqord2  11741  divneg  11902  div2neg  11933  recgt0  12056  infrenegsup  12193  supminf  12915  mul2lt0rlt0  13072  ceilval  13799  dfceil2  13800  ceilid  13812  modcyc2  13868  monoord2  13995  expval  14025  discr  14199  reneg  15068  imneg  15076  cjcj  15083  cjneg  15090  sqeqd  15109  telfsumo2  15745  infcvgaux1i  15799  infcvgaux2i  15800  risefallfac  15964  bpoly3  15998  sinneg  16085  tanneg  16087  sincossq  16115  odd2np1  16280  oexpneg  16284  modgcd  16470  pcneg  16803  mulgval  18948  mulgneg  18966  psgnunilem2  19357  evth2  24467  ivth2  24963  mbfposb  25161  mbfinf  25173  mbfi1flimlem  25231  iblcnlem  25297  iblrelem  25299  itgrevallem1  25303  iblneg  25311  itgneg  25312  ibladd  25329  ditgeq1  25356  ditgeq2  25357  ditgeq3  25358  ditgneg  25365  ditgswap  25367  dvrec  25463  dvrecg  25481  dvmptdiv  25482  dvexp3  25486  dvsincos  25489  rolle  25498  dvivth  25518  dvfsumge  25530  dvfsumlem2  25535  dvfsum2  25542  ftc2ditg  25554  vieta1lem2  25815  vieta1  25816  aaliou3lem2  25847  aaliou3lem8  25849  aaliou3lem5  25851  aaliou3lem6  25852  aaliou3lem7  25853  aaliou3  25855  sinperlem  25981  efimpi  25992  ptolemy  25997  sineq0  26024  efeq1  26028  tanregt0  26039  efif1olem2  26043  lognegb  26089  logneg2  26114  advlogexp  26154  logtayl  26159  logtayl2  26161  logccv  26162  cxpmul2z  26190  logbrec  26276  cosangneg2d  26301  isosctrlem2  26313  isosctrlem3  26314  angpined  26324  dcubic1lem  26337  dcubic2  26338  mcubic  26341  cubic2  26342  dquart  26347  quart1lem  26349  quartlem1  26351  quart  26355  asinlem3a  26364  asinneg  26380  atanneg  26401  atancj  26404  atanlogaddlem  26407  atanlogsublem  26409  atantan  26417  atantayl  26431  birthdaylem3  26447  amgmlem  26483  emcllem7  26495  lgamgulmlem2  26523  ftalem5  26570  basellem5  26578  basellem9  26582  lgsneg1  26814  lgseisenlem1  26867  lgseisenlem4  26870  m1lgs  26880  2sqblem  26923  dchrisum0flblem1  27000  rpvmasum2  27004  pntrsumo1  27057  pntrlog2bndlem2  27070  pntibndlem2  27083  padicfval  27108  padicval  27109  ostth3  27130  brbtwn2  28152  colinearalglem4  28156  axsegconlem9  28172  ex-ceil  29690  nvabs  29912  ipasslem2  30072  numdenneg  32010  archirngz  32322  ccfldextdgrr  32734  xrge0iifcv  32902  xrge0iifhom  32905  xrge0iif1  32906  xrge0tmd  32913  xrge0tmdALT  32914  fdvneggt  33600  fdvnegge  33602  climlec3  34691  gg-dvfsumlem2  35171  dvtan  36526  itg2addnclem3  36529  ibladdnc  36533  ftc1anclem5  36553  ftc1anclem6  36554  areacirclem1  36564  areacirc  36569  dffltz  41372  3cubeslem3r  41410  pellexlem6  41557  pell1234qrdich  41584  rmxm1  41658  rmym1  41659  monotoddzzfi  41666  monotoddzz  41667  oddcomabszz  41668  acongeq12d  41703  acongeq  41707  sineq0ALT  43683  infnsuprnmpt  43940  supminfrnmpt  44141  supminfxr  44160  neglimc  44349  dvcosax  44628  itgsin0pilem1  44652  itgsinexplem1  44656  itgsincmulx  44676  stoweidlem13  44715  stirlinglem5  44780  dirkerper  44798  dirkertrigeqlem3  44802  fourierdlem39  44848  fourierdlem40  44849  fourierdlem41  44850  fourierdlem43  44852  fourierdlem49  44857  fourierdlem73  44881  fourierdlem78  44886  fourierdlem103  44911  sqwvfourb  44931  etransclem46  44982  etransclem47  44983  sigarac  45554  sigaras  45557  sigarms  45558  sigariz  45565  sigarcol  45566  sharhght  45567  sigaradd  45568  2pwp1prm  46243  oexpnegALTV  46331  oexpnegnz  46332  itschlc0yqe  47399  itsclc0yqsol  47403  itsclquadb  47415  itscnhlinecirc02plem2  47422  amgmwlem  47802