Theorem negeqi 11409

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

Syntax hints:   = wceq 1550  -cneg 11401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384  df-neg 11403

This theorem is referenced by:  negsubdii  11502  recgt0ii  12084  m1expcl2  14084  crreczi  14227  absi  15285  geo2sum2  15876  bpoly2  16059  bpoly3  16060  sinhval  16158  coshval  16159  cos2bnd  16192  divalglem2  16401  m1expaddsub  19510  cnmsgnsubg  21598  psgninv  21603  ncvspi  25187  cphipval2  25272  ditg0  25884  cbvditg  25885  ang180lem2  26841  ang180lem3  26842  ang180lem4  26843  1cubrlem  26872  dcubic2  26875  atandm2  26908  efiasin  26919  asinsinlem  26922  asinsin  26923  asin1  26925  reasinsin  26927  atancj  26941  atantayl2  26969  ppiub  27234  lgseisenlem1  27405  lgseisenlem2  27406  lgsquadlem1  27410  ostth3  27668  nvpi  30805  ipidsq  30848  ipasslem10  30977  normlem1  31248  polid2i  31295  lnophmlem2  32155  archirngz  33319  cos9thpiminplylem1  34023  cos9thpiminplylem5  34027  xrge0iif1  34179  ballotlem2  34730  ditgeq123i  36507  cbvditgvw2  36547  itg2addnclem3  38110  dvasin  38141  areacirc  38150  cos2t3rdpi  42901  sin4t3rdpi  42902  cos4t3rdpi  42903  lhe4.4ex1a  44843  itgsin0pilem1  46462  stoweidlem26  46538  dirkertrigeqlem3  46612  fourierdlem103  46721  sqwvfourb  46741  fourierswlem  46742  proththd  48161