Theorem negeqd 10727

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

Syntax hints:   → wi 4   = wceq 1522  -cneg 10718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-iota 6189  df-fv 6233  df-ov 7019  df-neg 10720

This theorem is referenced by:  negdi  10791  mulneg2  10925  mulm1  10929  ltord2  11017  leord2  11018  eqord2  11019  divneg  11180  div2neg  11211  recgt0  11334  infrenegsup  11472  supminf  12184  mul2lt0rlt0  12341  ceilval  13058  dfceil2  13059  ceilid  13069  modcyc2  13125  monoord2  13251  expval  13281  discr  13451  reneg  14318  imneg  14326  cjcj  14333  cjneg  14340  sqeqd  14359  telfsumo2  14991  infcvgaux1i  15045  infcvgaux2i  15046  risefallfac  15211  bpoly3  15245  sinneg  15332  tanneg  15334  sincossq  15362  odd2np1  15523  oexpneg  15527  modgcd  15713  pcneg  16039  mulgval  17985  mulgneg  18001  psgnunilem2  18354  evth2  23247  ivth2  23739  mbfposb  23937  mbfinf  23949  mbfi1flimlem  24006  iblcnlem  24072  iblrelem  24074  itgrevallem1  24078  iblneg  24086  itgneg  24087  ibladd  24104  ditgeq1  24129  ditgeq2  24130  ditgeq3  24131  ditgneg  24138  ditgswap  24140  dvrec  24235  dvrecg  24253  dvmptdiv  24254  dvexp3  24258  dvsincos  24261  rolle  24270  dvivth  24290  dvfsumge  24302  dvfsumlem2  24307  dvfsum2  24314  ftc2ditg  24326  vieta1lem2  24583  vieta1  24584  aaliou3lem2  24615  aaliou3lem8  24617  aaliou3lem5  24619  aaliou3lem6  24620  aaliou3lem7  24621  aaliou3  24623  sinperlem  24749  efimpi  24760  ptolemy  24765  sineq0  24792  efeq1  24794  tanregt0  24804  efif1olem2  24808  lognegb  24854  logneg2  24879  advlogexp  24919  logtayl  24924  logtayl2  24926  logccv  24927  cxpmul2z  24955  logbrec  25041  cosangneg2d  25066  isosctrlem2  25078  isosctrlem3  25079  angpined  25089  dcubic1lem  25102  dcubic2  25103  mcubic  25106  cubic2  25107  dquart  25112  quart1lem  25114  quartlem1  25116  quart  25120  asinlem3a  25129  asinneg  25145  atanneg  25166  atancj  25169  atanlogaddlem  25172  atanlogsublem  25174  atantan  25182  atantayl  25196  birthdaylem3  25213  amgmlem  25249  emcllem7  25261  lgamgulmlem2  25289  ftalem5  25336  basellem5  25344  basellem9  25348  lgsneg1  25580  lgseisenlem1  25633  lgseisenlem4  25636  m1lgs  25646  2sqblem  25689  dchrisum0flblem1  25766  rpvmasum2  25770  pntrsumo1  25823  pntrlog2bndlem2  25836  pntibndlem2  25849  padicfval  25874  padicval  25875  ostth3  25896  brbtwn2  26374  colinearalglem4  26378  axsegconlem9  26394  ex-ceil  27919  nvabs  28140  ipasslem2  28300  numdenneg  30217  archirngz  30456  ccfldextdgrr  30661  xrge0iifcv  30794  xrge0iifhom  30797  xrge0iif1  30798  xrge0tmd  30805  xrge0tmdALT  30806  fdvneggt  31488  fdvnegge  31490  climlec3  32573  dvtan  34473  itg2addnclem3  34476  ibladdnc  34480  ftc1anclem5  34502  ftc1anclem6  34503  areacirclem1  34513  areacirc  34518  dffltz  38768  pellexlem6  38916  pell1234qrdich  38943  rmxm1  39016  rmym1  39017  monotoddzzfi  39024  monotoddzz  39025  oddcomabszz  39026  acongeq12d  39061  acongeq  39065  sineq0ALT  40810  infnsuprnmpt  41063  supminfrnmpt  41261  supminfxr  41282  neglimc  41470  dvcosax  41752  itgsin0pilem1  41776  itgsinexplem1  41780  itgsincmulx  41800  stoweidlem13  41840  stirlinglem5  41905  dirkerper  41923  dirkertrigeqlem3  41927  fourierdlem39  41973  fourierdlem40  41974  fourierdlem41  41975  fourierdlem43  41977  fourierdlem49  41982  fourierdlem73  42006  fourierdlem78  42011  fourierdlem103  42036  sqwvfourb  42056  etransclem46  42107  etransclem47  42108  sigarac  42651  sigaras  42654  sigarms  42655  sigariz  42662  sigarcol  42663  sharhght  42664  sigaradd  42665  2pwp1prm  43233  oexpnegALTV  43324  oexpnegnz  43325  itschlc0yqe  44228  itsclc0yqsol  44232  itsclquadb  44244  itscnhlinecirc02plem2  44251  amgmwlem  44383