cu2

		Ref	Expression
	Assertion	cu2	$⊢ 2^{3} = 8$

Step	Hyp	Ref	Expression
1		df-3	$⊢ 3 = 2 + 1$
2	1	oveq2i	$⊢ 2^{3} = 2^{2 + 1}$
3		2cn	$⊢ 2 \in ℂ$
4		2nn0	$⊢ 2 \in ℕ_{0}$
5		expp1	$⊢ (2 \in ℂ \land 2 \in ℕ_{0}) \to 2^{2 + 1} = 2^{2} \cdot 2$
6	3 4 5	mp2an	$⊢ 2^{2 + 1} = 2^{2} \cdot 2$
7		sq2	$⊢ 2^{2} = 4$
8	7	oveq1i	$⊢ 2^{2} \cdot 2 = 4 \cdot 2$
9		4t2e8	$⊢ 4 \cdot 2 = 8$
10	8 9	eqtri	$⊢ 2^{2} \cdot 2 = 8$
11	6 10	eqtri	$⊢ 2^{2 + 1} = 8$
12	2 11	eqtri	$⊢ 2^{3} = 8$

Metamath Proof Explorer