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