Metamath Proof Explorer

Theorem negeqi

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

Ref Expression
Hypothesis negeqi.1 
|- A = B
Assertion negeqi 
|- -u A = -u B

Proof

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