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\left(2+1\right)$$
3		3cn	$$⊢3\in ℂ$$
4		2cn	$$⊢2\in ℂ$$
5		ax-1cn	$$⊢1\in ℂ$$
6	3 4 5	adddii	$$⊢3\left(2+1\right)=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\left(2+1\right)=6+3$$
11		6p3e9	$$⊢6+3=9$$
12	10 11	eqtri	$$⊢3\left(2+1\right)=9$$
13	2 12	eqtri	$$⊢3\cdot 3=9$$