Theorem negeqi 11144

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

Syntax hints:   = wceq 1539  -cneg 11136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138

This theorem is referenced by:  negsubdii  11236  recgt0ii  11811  m1expcl2  13732  crreczi  13871  absi  14926  geo2sum2  15514  bpoly2  15695  bpoly3  15696  sinhval  15791  coshval  15792  cos2bnd  15825  divalglem2  16032  m1expaddsub  19021  cnmsgnsubg  20694  psgninv  20699  ncvspi  24225  cphipval2  24310  ditg0  24922  cbvditg  24923  ang180lem2  25865  ang180lem3  25866  ang180lem4  25867  1cubrlem  25896  dcubic2  25899  atandm2  25932  efiasin  25943  asinsinlem  25946  asinsin  25947  asin1  25949  reasinsin  25951  atancj  25965  atantayl2  25993  ppiub  26257  lgseisenlem1  26428  lgseisenlem2  26429  lgsquadlem1  26433  ostth3  26691  nvpi  28930  ipidsq  28973  ipasslem10  29102  normlem1  29373  polid2i  29420  lnophmlem2  30280  archirngz  31345  xrge0iif1  31790  ballotlem2  32355  itg2addnclem3  35757  dvasin  35788  areacirc  35797  lhe4.4ex1a  41836  itgsin0pilem1  43381  stoweidlem26  43457  dirkertrigeqlem3  43531  fourierdlem103  43640  sqwvfourb  43660  fourierswlem  43661  proththd  44954