Theorem negeqi 11457

Description: Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
negeqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
negeqi	⊢ -𝐴 = -𝐵

Proof of Theorem negeqi

Step	Hyp	Ref	Expression
1		negeqi.1	. 2 ⊢ 𝐴 = 𝐵
2		negeq 11456	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	ax-mp 5	1 ⊢ -𝐴 = -𝐵

Syntax hints:   = wceq 1541  -cneg 11449

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-neg 11451

This theorem is referenced by:  negsubdii  11549  recgt0ii  12124  m1expcl2  14055  crreczi  14195  absi  15237  geo2sum2  15824  bpoly2  16005  bpoly3  16006  sinhval  16101  coshval  16102  cos2bnd  16135  divalglem2  16342  m1expaddsub  19407  cnmsgnsubg  21349  psgninv  21354  ncvspi  24897  cphipval2  24982  ditg0  25594  cbvditg  25595  ang180lem2  26539  ang180lem3  26540  ang180lem4  26541  1cubrlem  26570  dcubic2  26573  atandm2  26606  efiasin  26617  asinsinlem  26620  asinsin  26621  asin1  26623  reasinsin  26625  atancj  26639  atantayl2  26667  ppiub  26931  lgseisenlem1  27102  lgseisenlem2  27103  lgsquadlem1  27107  ostth3  27365  nvpi  30175  ipidsq  30218  ipasslem10  30347  normlem1  30618  polid2i  30665  lnophmlem2  31525  archirngz  32593  xrge0iif1  33204  ballotlem2  33773  itg2addnclem3  36844  dvasin  36875  areacirc  36884  lhe4.4ex1a  43390  itgsin0pilem1  44965  stoweidlem26  45041  dirkertrigeqlem3  45115  fourierdlem103  45224  sqwvfourb  45244  fourierswlem  45245  proththd  46581