Theorem negeqi 11385

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

Syntax hints:   = wceq 1542  -cneg 11377

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379

This theorem is referenced by:  negsubdii  11478  recgt0ii  12060  m1expcl2  14020  crreczi  14163  absi  15221  geo2sum2  15809  bpoly2  15992  bpoly3  15993  sinhval  16091  coshval  16092  cos2bnd  16125  divalglem2  16334  m1expaddsub  19442  cnmsgnsubg  21547  psgninv  21552  ncvspi  25127  cphipval2  25212  ditg0  25825  cbvditg  25826  ang180lem2  26791  ang180lem3  26792  ang180lem4  26793  1cubrlem  26822  dcubic2  26825  atandm2  26858  efiasin  26869  asinsinlem  26872  asinsin  26873  asin1  26875  reasinsin  26877  atancj  26891  atantayl2  26919  ppiub  27186  lgseisenlem1  27357  lgseisenlem2  27358  lgsquadlem1  27362  ostth3  27620  nvpi  30759  ipidsq  30802  ipasslem10  30931  normlem1  31202  polid2i  31249  lnophmlem2  32109  archirngz  33287  cos9thpiminplylem1  33964  cos9thpiminplylem5  33968  xrge0iif1  34120  ballotlem2  34671  ditgeq123i  36429  cbvditgvw2  36469  itg2addnclem3  37928  dvasin  37959  areacirc  37968  cos2t3rdpi  42728  sin4t3rdpi  42729  cos4t3rdpi  42730  lhe4.4ex1a  44689  itgsin0pilem1  46312  stoweidlem26  46388  dirkertrigeqlem3  46462  fourierdlem103  46571  sqwvfourb  46591  fourierswlem  46592  proththd  47978