Metamath Proof Explorer


Theorem sqcl

Description: Closure of square. (Contributed by NM, 10-Aug-1999)

Ref Expression
Assertion sqcl A A 2

Proof

Step Hyp Ref Expression
1 sqval A A 2 = A A
2 mulcl A A A A
3 2 anidms A A A
4 1 3 eqeltrd A A 2