Metamath Proof Explorer

Theorem negnegd

Description: A number is equal to the negative of its negative. Theorem I.4 of Apostol p. 18. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypothesis negidd.1 φ A
Assertion negnegd φ A = A


Step Hyp Ref Expression
1 negidd.1 φ A
2 negneg A A = A
3 1 2 syl φ A = A