Theorem negeqi 11356

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 11355	. 2 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
3	1, 2	ax-mp 5	1 ⊢ -𝐴 = -𝐵

Syntax hints:   = wceq 1540  -cneg 11348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-neg 11350

This theorem is referenced by:  negsubdii  11449  recgt0ii  12031  m1expcl2  13992  crreczi  14135  absi  15193  geo2sum2  15781  bpoly2  15964  bpoly3  15965  sinhval  16063  coshval  16064  cos2bnd  16097  divalglem2  16306  m1expaddsub  19377  cnmsgnsubg  21484  psgninv  21489  ncvspi  25054  cphipval2  25139  ditg0  25752  cbvditg  25753  ang180lem2  26718  ang180lem3  26719  ang180lem4  26720  1cubrlem  26749  dcubic2  26752  atandm2  26785  efiasin  26796  asinsinlem  26799  asinsin  26800  asin1  26802  reasinsin  26804  atancj  26818  atantayl2  26846  ppiub  27113  lgseisenlem1  27284  lgseisenlem2  27285  lgsquadlem1  27289  ostth3  27547  nvpi  30611  ipidsq  30654  ipasslem10  30783  normlem1  31054  polid2i  31101  lnophmlem2  31961  archirngz  33132  cos9thpiminplylem1  33755  cos9thpiminplylem5  33759  xrge0iif1  33911  ballotlem2  34463  ditgeq123i  36193  cbvditgvw2  36233  itg2addnclem3  37663  dvasin  37694  areacirc  37703  cos2t3rdpi  42337  sin4t3rdpi  42338  cos4t3rdpi  42339  lhe4.4ex1a  44312  itgsin0pilem1  45941  stoweidlem26  46017  dirkertrigeqlem3  46091  fourierdlem103  46200  sqwvfourb  46220  fourierswlem  46221  proththd  47608