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

Metamath Proof Explorer

Theorem 3exp3

Description: Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015)

		Ref	Expression
	Assertion	3exp3	$⊢ 3^{3} = 27$

Step	Hyp	Ref	Expression
1		3nn0	$⊢ 3 \in ℕ_{0}$
2		2nn0	$⊢ 2 \in ℕ_{0}$
3		2p1e3	$⊢ 2 + 1 = 3$
4		sq3	$⊢ 3^{2} = 9$
5	4	oveq1i	$⊢ 3^{2} \cdot 3 = 9 \cdot 3$
6		9t3e27	$⊢ 9 \cdot 3 = 27$
7	5 6	eqtri	$⊢ 3^{2} \cdot 3 = 27$
8	1 2 3 7	numexpp1	$⊢ 3^{3} = 27$