Theorem negeqi 11453

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

Syntax hints:   = wceq 1542  -cneg 11445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447

This theorem is referenced by:  negsubdii  11545  recgt0ii  12120  m1expcl2  14051  crreczi  14191  absi  15233  geo2sum2  15820  bpoly2  16001  bpoly3  16002  sinhval  16097  coshval  16098  cos2bnd  16131  divalglem2  16338  m1expaddsub  19366  cnmsgnsubg  21130  psgninv  21135  ncvspi  24673  cphipval2  24758  ditg0  25370  cbvditg  25371  ang180lem2  26315  ang180lem3  26316  ang180lem4  26317  1cubrlem  26346  dcubic2  26349  atandm2  26382  efiasin  26393  asinsinlem  26396  asinsin  26397  asin1  26399  reasinsin  26401  atancj  26415  atantayl2  26443  ppiub  26707  lgseisenlem1  26878  lgseisenlem2  26879  lgsquadlem1  26883  ostth3  27141  nvpi  29920  ipidsq  29963  ipasslem10  30092  normlem1  30363  polid2i  30410  lnophmlem2  31270  archirngz  32335  xrge0iif1  32918  ballotlem2  33487  itg2addnclem3  36541  dvasin  36572  areacirc  36581  lhe4.4ex1a  43088  itgsin0pilem1  44666  stoweidlem26  44742  dirkertrigeqlem3  44816  fourierdlem103  44925  sqwvfourb  44945  fourierswlem  44946  proththd  46282