Theorem negeqi 11390

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

Syntax hints:   = wceq 1540  -cneg 11382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-neg 11384

This theorem is referenced by:  negsubdii  11483  recgt0ii  12065  m1expcl2  14026  crreczi  14169  absi  15228  geo2sum2  15816  bpoly2  15999  bpoly3  16000  sinhval  16098  coshval  16099  cos2bnd  16132  divalglem2  16341  m1expaddsub  19412  cnmsgnsubg  21519  psgninv  21524  ncvspi  25089  cphipval2  25174  ditg0  25787  cbvditg  25788  ang180lem2  26753  ang180lem3  26754  ang180lem4  26755  1cubrlem  26784  dcubic2  26787  atandm2  26820  efiasin  26831  asinsinlem  26834  asinsin  26835  asin1  26837  reasinsin  26839  atancj  26853  atantayl2  26881  ppiub  27148  lgseisenlem1  27319  lgseisenlem2  27320  lgsquadlem1  27324  ostth3  27582  nvpi  30646  ipidsq  30689  ipasslem10  30818  normlem1  31089  polid2i  31136  lnophmlem2  31996  archirngz  33158  cos9thpiminplylem1  33765  cos9thpiminplylem5  33769  xrge0iif1  33921  ballotlem2  34473  ditgeq123i  36190  cbvditgvw2  36230  itg2addnclem3  37660  dvasin  37691  areacirc  37700  cos2t3rdpi  42335  sin4t3rdpi  42336  cos4t3rdpi  42337  lhe4.4ex1a  44311  itgsin0pilem1  45941  stoweidlem26  46017  dirkertrigeqlem3  46091  fourierdlem103  46200  sqwvfourb  46220  fourierswlem  46221  proththd  47608