Theorem negeqi 10868

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

Syntax hints:   = wceq 1538  -cneg 10860

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-neg 10862

This theorem is referenced by:  negsubdii  10960  recgt0ii  11535  m1expcl2  13447  crreczi  13585  absi  14638  geo2sum2  15222  bpoly2  15403  bpoly3  15404  sinhval  15499  coshval  15500  cos2bnd  15533  divalglem2  15736  m1expaddsub  18618  cnmsgnsubg  20266  psgninv  20271  ncvspi  23761  cphipval2  23845  ditg0  24456  cbvditg  24457  ang180lem2  25396  ang180lem3  25397  ang180lem4  25398  1cubrlem  25427  dcubic2  25430  atandm2  25463  efiasin  25474  asinsinlem  25477  asinsin  25478  asin1  25480  reasinsin  25482  atancj  25496  atantayl2  25524  ppiub  25788  lgseisenlem1  25959  lgseisenlem2  25960  lgsquadlem1  25964  ostth3  26222  nvpi  28450  ipidsq  28493  ipasslem10  28622  normlem1  28893  polid2i  28940  lnophmlem2  29800  archirngz  30868  xrge0iif1  31291  ballotlem2  31856  itg2addnclem3  35110  dvasin  35141  areacirc  35150  lhe4.4ex1a  41033  itgsin0pilem1  42592  stoweidlem26  42668  dirkertrigeqlem3  42742  fourierdlem103  42851  sqwvfourb  42871  fourierswlem  42872  proththd  44132