Theorem negeqi 11380

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

Syntax hints:   = wceq 1542  -cneg 11372

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-neg 11374

This theorem is referenced by:  negsubdii  11473  recgt0ii  12056  m1expcl2  14041  crreczi  14184  absi  15242  geo2sum2  15833  bpoly2  16016  bpoly3  16017  sinhval  16115  coshval  16116  cos2bnd  16149  divalglem2  16358  m1expaddsub  19467  cnmsgnsubg  21570  psgninv  21575  ncvspi  25136  cphipval2  25221  ditg0  25833  cbvditg  25834  ang180lem2  26790  ang180lem3  26791  ang180lem4  26792  1cubrlem  26821  dcubic2  26824  atandm2  26857  efiasin  26868  asinsinlem  26871  asinsin  26872  asin1  26874  reasinsin  26876  atancj  26890  atantayl2  26918  ppiub  27184  lgseisenlem1  27355  lgseisenlem2  27356  lgsquadlem1  27360  ostth3  27618  nvpi  30756  ipidsq  30799  ipasslem10  30928  normlem1  31199  polid2i  31246  lnophmlem2  32106  archirngz  33268  cos9thpiminplylem1  33945  cos9thpiminplylem5  33949  xrge0iif1  34101  ballotlem2  34652  ditgeq123i  36410  cbvditgvw2  36450  itg2addnclem3  38011  dvasin  38042  areacirc  38051  cos2t3rdpi  42803  sin4t3rdpi  42804  cos4t3rdpi  42805  lhe4.4ex1a  44777  itgsin0pilem1  46399  stoweidlem26  46475  dirkertrigeqlem3  46549  fourierdlem103  46658  sqwvfourb  46678  fourierswlem  46679  proththd  48092