Metamath Proof Explorer

Theorem xnegnegi

Description: Extended real version of negneg . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis xnegnegi.1 
|- A e. RR*
Assertion xnegnegi 
|- -e -e A = A

Proof

Step Hyp Ref Expression
1 xnegnegi.1 
 |-  A e. RR*
2 xnegneg 
 |-  ( A e. RR* -> -e -e A = A )
3 1 2 ax-mp 
 |-  -e -e A = A