Metamath Proof Explorer


Theorem sqcli

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

Ref Expression
Hypothesis sqval.1 A
Assertion sqcli A 2

Proof

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