Metamath Proof Explorer

Theorem negeqd

Description: Equality deduction for negatives. (Contributed by NM, 14-May-1999)

Ref Expression
Hypothesis negeqd.1 
|- ( ph -> A = B )
Assertion negeqd 
|- ( ph -> -u A = -u B )

Proof

Step Hyp Ref Expression
1 negeqd.1 
 |-  ( ph -> A = B )
2 negeq 
 |-  ( A = B -> -u A = -u B )
3 1 2 syl 
 |-  ( ph -> -u A = -u B )