Theorem negeqi 11344

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

Syntax hints:   = wceq 1540  -cneg 11336

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 3393  df-v 3435  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-iota 6432  df-fv 6484  df-ov 7343  df-neg 11338

This theorem is referenced by:  negsubdii  11437  recgt0ii  12019  m1expcl2  13980  crreczi  14123  absi  15180  geo2sum2  15768  bpoly2  15951  bpoly3  15952  sinhval  16050  coshval  16051  cos2bnd  16084  divalglem2  16293  m1expaddsub  19364  cnmsgnsubg  21468  psgninv  21473  ncvspi  25037  cphipval2  25122  ditg0  25735  cbvditg  25736  ang180lem2  26701  ang180lem3  26702  ang180lem4  26703  1cubrlem  26732  dcubic2  26735  atandm2  26768  efiasin  26779  asinsinlem  26782  asinsin  26783  asin1  26785  reasinsin  26787  atancj  26801  atantayl2  26829  ppiub  27096  lgseisenlem1  27267  lgseisenlem2  27268  lgsquadlem1  27272  ostth3  27530  nvpi  30598  ipidsq  30641  ipasslem10  30770  normlem1  31041  polid2i  31088  lnophmlem2  31948  archirngz  33126  cos9thpiminplylem1  33763  cos9thpiminplylem5  33767  xrge0iif1  33919  ballotlem2  34470  ditgeq123i  36200  cbvditgvw2  36240  itg2addnclem3  37670  dvasin  37701  areacirc  37710  cos2t3rdpi  42344  sin4t3rdpi  42345  cos4t3rdpi  42346  lhe4.4ex1a  44319  itgsin0pilem1  45945  stoweidlem26  46021  dirkertrigeqlem3  46095  fourierdlem103  46204  sqwvfourb  46224  fourierswlem  46225  proththd  47612