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 φ A 2 = A 2

Proof

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