Theorem negeqi 10274

Description: Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
negeqi.1	|- A = B

Assertion

Ref	Expression
negeqi	|- -u A = -u B

Proof of Theorem negeqi

Step	Hyp	Ref	Expression
1		negeqi.1	. 2 |- A = B
2		negeq 10273	. 2 |- ( A = B -> -u A = -u B )
3	1, 2	ax-mp 5	1 |- -u A = -u B

Syntax hints:   = wceq 1483   -ucneg 10267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269

This theorem is referenced by:  negsubdii  10366  recgt0ii  10929  m1expcl2  12882  crreczi  12989  absi  14026  geo2sum2  14605  bpoly2  14788  bpoly3  14789  sinhval  14884  coshval  14885  cos2bnd  14918  divalglem2  15118  m1expaddsub  17918  cnmsgnsubg  19923  psgninv  19928  ncvspi  22956  cphipval2  23040  ditg0  23617  cbvditg  23618  ang180lem2  24540  ang180lem3  24541  ang180lem4  24542  1cubrlem  24568  dcubic2  24571  atandm2  24604  efiasin  24615  asinsinlem  24618  asinsin  24619  asin1  24621  reasinsin  24623  atancj  24637  atantayl2  24665  ppiub  24929  lgseisenlem1  25100  lgseisenlem2  25101  lgsquadlem1  25105  ostth3  25327  nvpi  27522  ipidsq  27565  ipasslem10  27694  normlem1  27967  polid2i  28014  lnophmlem2  28876  archirngz  29743  xrge0iif1  29984  ballotlem2  30550  itg2addnclem3  33463  dvasin  33496  areacirc  33505  lhe4.4ex1a  38528  itgsin0pilem1  40165  stoweidlem26  40243  dirkertrigeqlem3  40317  fourierdlem103  40426  sqwvfourb  40446  fourierswlem  40447  proththd  41531