Theorem negeqi 11423

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

Syntax hints:   = wceq 1560  -cneg 11415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-neg 11417

This theorem is referenced by:  negsubdii  11516  recgt0ii  12098  m1expcl2  14098  crreczi  14241  absi  15313  geo2sum2  15904  bpoly2  16087  bpoly3  16088  sinhval  16186  coshval  16187  cos2bnd  16220  divalglem2  16429  m1expaddsub  19538  cnmsgnsubg  21629  psgninv  21634  ncvspi  25218  cphipval2  25303  ditg0  25915  cbvditg  25916  ang180lem2  26875  ang180lem3  26876  ang180lem4  26877  1cubrlem  26906  dcubic2  26909  atandm2  26942  efiasin  26953  asinsinlem  26956  asinsin  26957  asin1  26959  reasinsin  26961  atancj  26975  atantayl2  27003  ppiub  27268  lgseisenlem1  27439  lgseisenlem2  27440  lgsquadlem1  27444  ostth3  27702  nvpi  30870  ipidsq  30913  ipasslem10  31042  normlem1  31313  polid2i  31360  lnophmlem2  32220  archirngz  33369  cos9thpiminplylem1  34079  cos9thpiminplylem5  34083  xrge0iif1  34235  ballotlem2  34786  ditgeq123i  36569  cbvditgvw2  36609  itg2addnclem3  38172  dvasin  38203  areacirc  38212  cos2t3rdpi  42963  sin4t3rdpi  42964  cos4t3rdpi  42965  lhe4.4ex1a  44905  itgsin0pilem1  46524  stoweidlem26  46600  dirkertrigeqlem3  46674  fourierdlem103  46783  sqwvfourb  46803  fourierswlem  46804  proththd  48223