Theorem negeqi 11432

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

Syntax hints:   = wceq 1541  -cneg 11424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3430  df-v 3472  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4520  df-sn 4620  df-pr 4622  df-op 4626  df-uni 4899  df-br 5139  df-iota 6481  df-fv 6537  df-ov 7393  df-neg 11426

This theorem is referenced by:  negsubdii  11524  recgt0ii  12099  m1expcl2  14030  crreczi  14170  absi  15212  geo2sum2  15799  bpoly2  15980  bpoly3  15981  sinhval  16076  coshval  16077  cos2bnd  16110  divalglem2  16317  m1expaddsub  19327  cnmsgnsubg  21058  psgninv  21063  ncvspi  24597  cphipval2  24682  ditg0  25294  cbvditg  25295  ang180lem2  26237  ang180lem3  26238  ang180lem4  26239  1cubrlem  26268  dcubic2  26271  atandm2  26304  efiasin  26315  asinsinlem  26318  asinsin  26319  asin1  26321  reasinsin  26323  atancj  26337  atantayl2  26365  ppiub  26629  lgseisenlem1  26800  lgseisenlem2  26801  lgsquadlem1  26805  ostth3  27063  nvpi  29778  ipidsq  29821  ipasslem10  29950  normlem1  30221  polid2i  30268  lnophmlem2  31128  archirngz  32201  xrge0iif1  32733  ballotlem2  33302  itg2addnclem3  36329  dvasin  36360  areacirc  36369  lhe4.4ex1a  42845  itgsin0pilem1  44425  stoweidlem26  44501  dirkertrigeqlem3  44575  fourierdlem103  44684  sqwvfourb  44704  fourierswlem  44705  proththd  46040