Metamath Proof Explorer


Theorem sqnegd

Description: The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024)

Ref Expression
Hypothesis sqnegd.1 φA
Assertion sqnegd φA2=A2

Proof

Step Hyp Ref Expression
1 sqnegd.1 φA
2 sqneg AA2=A2
3 1 2 syl φA2=A2