Theorem negeqi 11449

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

Syntax hints:   = wceq 1533  -cneg 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404  df-neg 11443

This theorem is referenced by:  negsubdii  11541  recgt0ii  12116  m1expcl2  14047  crreczi  14187  absi  15229  geo2sum2  15816  bpoly2  15997  bpoly3  15998  sinhval  16093  coshval  16094  cos2bnd  16127  divalglem2  16334  m1expaddsub  19403  cnmsgnsubg  21430  psgninv  21435  ncvspi  24994  cphipval2  25079  ditg0  25692  cbvditg  25693  ang180lem2  26646  ang180lem3  26647  ang180lem4  26648  1cubrlem  26677  dcubic2  26680  atandm2  26713  efiasin  26724  asinsinlem  26727  asinsin  26728  asin1  26730  reasinsin  26732  atancj  26746  atantayl2  26774  ppiub  27041  lgseisenlem1  27212  lgseisenlem2  27213  lgsquadlem1  27217  ostth3  27475  nvpi  30344  ipidsq  30387  ipasslem10  30516  normlem1  30787  polid2i  30834  lnophmlem2  31694  archirngz  32762  xrge0iif1  33373  ballotlem2  33942  itg2addnclem3  36997  dvasin  37028  areacirc  37037  lhe4.4ex1a  43543  itgsin0pilem1  45117  stoweidlem26  45193  dirkertrigeqlem3  45267  fourierdlem103  45376  sqwvfourb  45396  fourierswlem  45397  proththd  46733