Theorem negeqi 11450

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

Syntax hints:   = wceq 1567  -cneg 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-neg 11444

This theorem is referenced by:  negsubdii  11543  recgt0ii  12121  m1expcl2  14121  crreczi  14264  absi  15337  geo2sum2  15928  bpoly2  16111  bpoly3  16112  sinhval  16210  coshval  16211  cos2bnd  16244  divalglem2  16453  m1expaddsub  19568  cnmsgnsubg  21696  psgninv  21701  ncvspi  25284  cphipval2  25369  ditg0  25981  cbvditg  25982  ang180lem2  26941  ang180lem3  26942  ang180lem4  26943  1cubrlem  26972  dcubic2  26975  atandm2  27008  efiasin  27019  asinsinlem  27022  asinsin  27023  asin1  27025  reasinsin  27027  atancj  27041  atantayl2  27069  ppiub  27334  lgseisenlem1  27505  lgseisenlem2  27506  lgsquadlem1  27510  ostth3  27768  nvpi  30960  ipidsq  31003  ipasslem10  31132  normlem1  31403  polid2i  31450  lnophmlem2  32310  archirngz  33450  cos9thpiminplylem1  34117  cos9thpiminplylem5  34121  xrge0iif1  34273  ballotlem2  34824  ditgeq123i  36610  cbvditgvw2  36650  itg2addnclem3  38212  dvasin  38243  areacirc  38252  25or6to4  42863  cos2t3rdpi  43005  sin4t3rdpi  43006  cos4t3rdpi  43007  lhe4.4ex1a  44931  itgsin0pilem1  46556  stoweidlem26  46632  dirkertrigeqlem3  46706  fourierdlem103  46815  sqwvfourb  46835  fourierswlem  46836  proththd  48255