Theorem negeqd 11381

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

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

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-neg 11374

This theorem is referenced by:  negdi  11445  mulneg2  11581  mulm1  11585  ltord2  11673  leord2  11674  eqord2  11675  divneg  11840  div2neg  11872  recgt0  11995  infrenegsup  12133  supminf  12879  mul2lt0rlt0  13040  ceilval  13791  dfceil2  13792  ceilid  13804  modcyc2  13860  monoord2  13989  expval  14019  discr  14196  reneg  15081  imneg  15089  cjcj  15096  cjneg  15103  sqeqd  15122  telfsumo2  15760  infcvgaux1i  15816  infcvgaux2i  15817  risefallfac  15983  bpoly3  16017  sinneg  16107  tanneg  16109  sincossq  16137  odd2np1  16304  oexpneg  16308  modgcd  16495  pcneg  16839  mulgval  19041  mulgneg  19062  psgnunilem2  19464  evth2  24940  ivth2  25435  mbfposb  25633  mbfinf  25645  mbfi1flimlem  25702  iblcnlem  25769  iblrelem  25771  itgrevallem1  25775  iblneg  25783  itgneg  25784  ibladd  25801  ditgeq1  25828  ditgeq2  25829  ditgeq3  25830  ditgneg  25837  ditgswap  25839  dvrec  25935  dvrecg  25953  dvmptdiv  25954  dvexp3  25958  dvsincos  25961  rolle  25970  dvivth  25990  dvfsumge  26002  dvfsumlem2  26007  dvfsum2  26014  ftc2ditg  26026  vieta1lem2  26291  vieta1  26292  aaliou3lem2  26323  aaliou3lem8  26325  aaliou3lem5  26327  aaliou3lem6  26328  aaliou3lem7  26329  aaliou3  26331  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  26762  cosangneg2d  26787  isosctrlem2  26799  isosctrlem3  26800  angpined  26810  dcubic1lem  26823  dcubic2  26824  mcubic  26827  cubic2  26828  dquart  26833  quart1lem  26835  quartlem1  26837  quart  26841  asinlem3a  26850  asinneg  26866  atanneg  26887  atancj  26890  atanlogaddlem  26893  atanlogsublem  26895  atantan  26903  atantayl  26917  birthdaylem3  26933  amgmlem  26970  emcllem7  26982  lgamgulmlem2  27010  ftalem5  27057  basellem5  27065  basellem9  27069  lgsneg1  27302  lgseisenlem1  27355  lgseisenlem4  27358  m1lgs  27368  2sqblem  27411  dchrisum0flblem1  27488  rpvmasum2  27492  pntrsumo1  27545  pntrlog2bndlem2  27558  pntibndlem2  27571  padicfval  27596  padicval  27597  ostth3  27618  brbtwn2  28991  colinearalglem4  28995  axsegconlem9  29011  ex-ceil  30536  nvabs  30761  ipasslem2  30921  sgnval2  32826  re0cj  32834  argcj  32839  numdenneg  32906  archirngz  33268  elrgspnlem1  33321  ccfldextdgrr  33835  constrrtcc  33898  constrnegcl  33926  constrrecl  33932  cos9thpiminplylem1  33945  cos9thpiminplylem2  33946  xrge0iifcv  34097  xrge0iifhom  34100  xrge0iif1  34101  xrge0tmd  34108  xrge0tmdALT  34109  fdvneggt  34763  fdvnegge  34765  climlec3  35935  ditgeq123dv  36422  cbvditgdavw  36483  cbvditgdavw2  36499  dvtan  38008  itg2addnclem3  38011  ibladdnc  38015  ftc1anclem5  38035  ftc1anclem6  38036  areacirclem1  38046  areacirc  38051  dffltz  43084  3cubeslem3r  43136  pellexlem6  43283  pell1234qrdich  43310  rmxm1  43383  rmym1  43384  monotoddzzfi  43391  monotoddzz  43392  oddcomabszz  43393  acongeq12d  43428  acongeq  43432  sineq0ALT  45384  infnsuprnmpt  45700  supminfrnmpt  45894  supminfxr  45913  neglimc  46096  dvcosax  46375  itgsin0pilem1  46399  itgsinexplem1  46403  itgsincmulx  46423  stoweidlem13  46462  stirlinglem5  46527  dirkerper  46545  dirkertrigeqlem3  46549  fourierdlem39  46595  fourierdlem40  46596  fourierdlem41  46597  fourierdlem43  46599  fourierdlem49  46604  fourierdlem73  46628  fourierdlem78  46633  fourierdlem103  46658  sqwvfourb  46678  etransclem46  46729  etransclem47  46730  sigarac  47301  sigaras  47304  sigarms  47305  sigariz  47312  sigarcol  47313  sharhght  47314  sigaradd  47315  nthrucw  47335  ceildivmod  47808  difmodm1lt  47828  2pwp1prm  48067  oexpnegALTV  48168  oexpnegnz  48169  itschlc0yqe  49251  itsclc0yqsol  49255  itsclquadb  49267  itscnhlinecirc02plem2  49274  amgmwlem  50292