This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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