Theorem 3t3e9

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

	Ref	Expression
Assertion	3t3e9	⊢ ( 3 · 3 ) = 9

Proof

Step	Hyp	Ref	Expression
1		df-3	⊢ 3 = ( 2 + 1 )
2	1	oveq2i	⊢ ( 3 · 3 ) = ( 3 · ( 2 + 1 ) )
3		3cn	⊢ 3 ∈ ℂ
4		2cn	⊢ 2 ∈ ℂ
5		ax-1cn	⊢ 1 ∈ ℂ
6	3 4 5	adddii	⊢ ( 3 · ( 2 + 1 ) ) = ( ( 3 · 2 ) + ( 3 · 1 ) )
7		3t2e6	⊢ ( 3 · 2 ) = 6
8		3t1e3	⊢ ( 3 · 1 ) = 3
9	7 8	oveq12i	⊢ ( ( 3 · 2 ) + ( 3 · 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 · 3 ) = 9