Theorem negeqi 11499

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

Syntax hints:   = wceq 1537  -cneg 11491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-neg 11493

This theorem is referenced by:  negsubdii  11592  recgt0ii  12172  m1expcl2  14123  crreczi  14264  absi  15322  geo2sum2  15907  bpoly2  16090  bpoly3  16091  sinhval  16187  coshval  16188  cos2bnd  16221  divalglem2  16429  m1expaddsub  19531  cnmsgnsubg  21613  psgninv  21618  ncvspi  25204  cphipval2  25289  ditg0  25903  cbvditg  25904  ang180lem2  26868  ang180lem3  26869  ang180lem4  26870  1cubrlem  26899  dcubic2  26902  atandm2  26935  efiasin  26946  asinsinlem  26949  asinsin  26950  asin1  26952  reasinsin  26954  atancj  26968  atantayl2  26996  ppiub  27263  lgseisenlem1  27434  lgseisenlem2  27435  lgsquadlem1  27439  ostth3  27697  nvpi  30696  ipidsq  30739  ipasslem10  30868  normlem1  31139  polid2i  31186  lnophmlem2  32046  archirngz  33179  xrge0iif1  33899  ballotlem2  34470  ditgeq123i  36191  cbvditgvw2  36232  itg2addnclem3  37660  dvasin  37691  areacirc  37700  lhe4.4ex1a  44325  itgsin0pilem1  45906  stoweidlem26  45982  dirkertrigeqlem3  46056  fourierdlem103  46165  sqwvfourb  46185  fourierswlem  46186  proththd  47539