Theorem negeqi 11386

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

Syntax hints:   = wceq 1542  -cneg 11378

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380

This theorem is referenced by:  negsubdii  11479  recgt0ii  12062  m1expcl2  14047  crreczi  14190  absi  15248  geo2sum2  15839  bpoly2  16022  bpoly3  16023  sinhval  16121  coshval  16122  cos2bnd  16155  divalglem2  16364  m1expaddsub  19473  cnmsgnsubg  21557  psgninv  21562  ncvspi  25123  cphipval2  25208  ditg0  25820  cbvditg  25821  ang180lem2  26774  ang180lem3  26775  ang180lem4  26776  1cubrlem  26805  dcubic2  26808  atandm2  26841  efiasin  26852  asinsinlem  26855  asinsin  26856  asin1  26858  reasinsin  26860  atancj  26874  atantayl2  26902  ppiub  27167  lgseisenlem1  27338  lgseisenlem2  27339  lgsquadlem1  27343  ostth3  27601  nvpi  30738  ipidsq  30781  ipasslem10  30910  normlem1  31181  polid2i  31228  lnophmlem2  32088  archirngz  33250  cos9thpiminplylem1  33926  cos9thpiminplylem5  33930  xrge0iif1  34082  ballotlem2  34633  ditgeq123i  36391  cbvditgvw2  36431  itg2addnclem3  37994  dvasin  38025  areacirc  38034  cos2t3rdpi  42786  sin4t3rdpi  42787  cos4t3rdpi  42788  lhe4.4ex1a  44756  itgsin0pilem1  46378  stoweidlem26  46454  dirkertrigeqlem3  46528  fourierdlem103  46637  sqwvfourb  46657  fourierswlem  46658  proththd  48077