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

Metamath Proof Explorer

Theorem 3t3e9

Description: 3 times 3 equals 9. (Contributed by NM, 11-May-2004)

		Ref	Expression
	Assertion	3t3e9	$⊢ 3 \cdot 3 = 9$

Proof

Step	Hyp	Ref	Expression
1		df-3	$⊢ 3 = 2 + 1$
2	1	oveq2i	$⊢ 3 \cdot 3 = 3 (2 + 1)$
3		3cn	$⊢ 3 \in ℂ$
4		2cn	$⊢ 2 \in ℂ$
5		ax-1cn	$⊢ 1 \in ℂ$
6	3 4 5	adddii	$⊢ 3 (2 + 1) = 3 \cdot 2 + 3 \cdot 1$
7		3t2e6	$⊢ 3 \cdot 2 = 6$
8		3t1e3	$⊢ 3 \cdot 1 = 3$
9	7 8	oveq12i	$⊢ 3 \cdot 2 + 3 \cdot 1 = 6 + 3$
10	6 9	eqtri	$⊢ 3 (2 + 1) = 6 + 3$
11		6p3e9	$⊢ 6 + 3 = 9$
12	10 11	eqtri	$⊢ 3 (2 + 1) = 9$
13	2 12	eqtri	$⊢ 3 \cdot 3 = 9$