Theorem negeqi 11212

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

Syntax hints:   = wceq 1542  -cneg 11204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-iota 6389  df-fv 6439  df-ov 7272  df-neg 11206

This theorem is referenced by:  negsubdii  11304  recgt0ii  11879  m1expcl2  13800  crreczi  13939  absi  14994  geo2sum2  15582  bpoly2  15763  bpoly3  15764  sinhval  15859  coshval  15860  cos2bnd  15893  divalglem2  16100  m1expaddsub  19102  cnmsgnsubg  20778  psgninv  20783  ncvspi  24316  cphipval2  24401  ditg0  25013  cbvditg  25014  ang180lem2  25956  ang180lem3  25957  ang180lem4  25958  1cubrlem  25987  dcubic2  25990  atandm2  26023  efiasin  26034  asinsinlem  26037  asinsin  26038  asin1  26040  reasinsin  26042  atancj  26056  atantayl2  26084  ppiub  26348  lgseisenlem1  26519  lgseisenlem2  26520  lgsquadlem1  26524  ostth3  26782  nvpi  29023  ipidsq  29066  ipasslem10  29195  normlem1  29466  polid2i  29513  lnophmlem2  30373  archirngz  31437  xrge0iif1  31882  ballotlem2  32449  itg2addnclem3  35824  dvasin  35855  areacirc  35864  lhe4.4ex1a  41915  itgsin0pilem1  43460  stoweidlem26  43536  dirkertrigeqlem3  43610  fourierdlem103  43719  sqwvfourb  43739  fourierswlem  43740  proththd  45033