Theorem negeqi 11430

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

Syntax hints:   = wceq 1541  -cneg 11422

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3429  df-v 3471  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-nul 4314  df-if 4518  df-sn 4618  df-pr 4620  df-op 4624  df-uni 4897  df-br 5137  df-iota 6479  df-fv 6535  df-ov 7391  df-neg 11424

This theorem is referenced by:  negsubdii  11522  recgt0ii  12097  m1expcl2  14028  crreczi  14168  absi  15210  geo2sum2  15797  bpoly2  15978  bpoly3  15979  sinhval  16074  coshval  16075  cos2bnd  16108  divalglem2  16315  m1expaddsub  19325  cnmsgnsubg  21056  psgninv  21061  ncvspi  24595  cphipval2  24680  ditg0  25292  cbvditg  25293  ang180lem2  26235  ang180lem3  26236  ang180lem4  26237  1cubrlem  26266  dcubic2  26269  atandm2  26302  efiasin  26313  asinsinlem  26316  asinsin  26317  asin1  26319  reasinsin  26321  atancj  26335  atantayl2  26363  ppiub  26627  lgseisenlem1  26798  lgseisenlem2  26799  lgsquadlem1  26803  ostth3  27061  nvpi  29729  ipidsq  29772  ipasslem10  29901  normlem1  30172  polid2i  30219  lnophmlem2  31079  archirngz  32152  xrge0iif1  32684  ballotlem2  33253  itg2addnclem3  36280  dvasin  36311  areacirc  36320  lhe4.4ex1a  42796  itgsin0pilem1  44376  stoweidlem26  44452  dirkertrigeqlem3  44526  fourierdlem103  44635  sqwvfourb  44655  fourierswlem  44656  proththd  45991