Metamath Proof Explorer


Theorem sq3

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

Ref Expression
Assertion sq3 3 2 = 9

Proof

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