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

Proof

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