Metamath Proof Explorer


Theorem sq3

Description: The square of 3 is 9. (Contributed by NM, 26-Apr-2006)

Ref Expression
Assertion sq3 32=9

Proof

Step Hyp Ref Expression
1 3cn 3
2 1 sqvali 32=33
3 3t3e9 33=9
4 2 3 eqtri 32=9