Metamath Proof Explorer


Theorem sqvali

Description: Value of square. Inference version. (Contributed by NM, 1-Aug-1999)

Ref Expression
Hypothesis sqval.1 A
Assertion sqvali A2=AA

Proof

Step Hyp Ref Expression
1 sqval.1 A
2 sqval AA2=AA
3 1 2 ax-mp A2=AA