Metamath Proof Explorer

Theorem xnegnegd

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

Ref Expression
Hypothesis xnegnegd.1 
|- ( ph -> A e. RR* )
Assertion xnegnegd 
|- ( ph -> -e -e A = A )

Proof

Step Hyp Ref Expression
1 xnegnegd.1 
 |-  ( ph -> A e. RR* )
2 xnegneg 
 |-  ( A e. RR* -> -e -e A = A )
3 1 2 syl 
 |-  ( ph -> -e -e A = A )