Metamath Proof Explorer


Theorem sqsqrti

Description: Square of square root. (Contributed by NM, 11-Aug-1999)

Ref Expression
Hypothesis sqrtthi.1 A
Assertion sqsqrti 0AA2=A

Proof

Step Hyp Ref Expression
1 sqrtthi.1 A
2 resqrtth A0AA2=A
3 1 2 mpan 0AA2=A