Metamath Proof Explorer


Theorem sqrtmsqi

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

Ref Expression
Hypothesis sqrtthi.1 A
Assertion sqrtmsqi 0AAA=A

Proof

Step Hyp Ref Expression
1 sqrtthi.1 A
2 sqrtmsq A0AAA=A
3 1 2 mpan 0AAA=A