Metamath Proof Explorer


Theorem xnegeqd

Description: Equality of two extended numbers with -e in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis xnegeqd.1
|- ( ph -> A = B )
Assertion xnegeqd
|- ( ph -> -e A = -e B )

Proof

Step Hyp Ref Expression
1 xnegeqd.1
 |-  ( ph -> A = B )
2 xnegeq
 |-  ( A = B -> -e A = -e B )
3 1 2 syl
 |-  ( ph -> -e A = -e B )