Theorem negeqi 11421

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

Syntax hints:   = wceq 1540  -cneg 11413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415

This theorem is referenced by:  negsubdii  11514  recgt0ii  12096  m1expcl2  14057  crreczi  14200  absi  15259  geo2sum2  15847  bpoly2  16030  bpoly3  16031  sinhval  16129  coshval  16130  cos2bnd  16163  divalglem2  16372  m1expaddsub  19435  cnmsgnsubg  21493  psgninv  21498  ncvspi  25063  cphipval2  25148  ditg0  25761  cbvditg  25762  ang180lem2  26727  ang180lem3  26728  ang180lem4  26729  1cubrlem  26758  dcubic2  26761  atandm2  26794  efiasin  26805  asinsinlem  26808  asinsin  26809  asin1  26811  reasinsin  26813  atancj  26827  atantayl2  26855  ppiub  27122  lgseisenlem1  27293  lgseisenlem2  27294  lgsquadlem1  27298  ostth3  27556  nvpi  30603  ipidsq  30646  ipasslem10  30775  normlem1  31046  polid2i  31093  lnophmlem2  31953  archirngz  33150  cos9thpiminplylem1  33779  cos9thpiminplylem5  33783  xrge0iif1  33935  ballotlem2  34487  ditgeq123i  36204  cbvditgvw2  36244  itg2addnclem3  37674  dvasin  37705  areacirc  37714  cos2t3rdpi  42349  sin4t3rdpi  42350  cos4t3rdpi  42351  lhe4.4ex1a  44325  itgsin0pilem1  45955  stoweidlem26  46031  dirkertrigeqlem3  46105  fourierdlem103  46214  sqwvfourb  46234  fourierswlem  46235  proththd  47619