Theorem negeqi 7013

Description: Equality inference for negatives.

Hypothesis

Ref	Expression
negeqi.1	|- A = B

Assertion

Ref	Expression
negeqi	|- -uA = -uB

Proof of Theorem negeqi

Step	Hyp	Ref	Expression
1		negeqi.1	. 2 |- A = B
2		negeq 7012	. 2 |- (A = B -> -uA = -uB)
3	1, 2	ax-mp 7	1 |- -uA = -uB

Syntax hints:   = wceq 1586  -ucneg 6990

This theorem is referenced by:  mulneg2i 7083  mul2negi 7084  negsubdii 7086  recgt0ii 7323  discrlem1 8290  sqrlem11 8317  crmuli 8374  crreczi 8375  imre 8407  renegi 8428  imnegi 8430  cjnegi 8431  cos2bnd 9139  divalglem2 9292  nvpi 10495  ipid 10571  ipasslem10 10709  pilem3 10893  eulerid 10903  pilog 10993  normlem1 11446  polid2i 11493  pjthlem5 11690  lnophmlem2 12411  mamb 15824

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-xp 4133  df-cnv 4135  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fv 4147  df-opr 4983  df-neg 7011

Copyright terms: Public domain