Theorem 3t3e9

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

	Ref	Expression
Assertion	3t3e9	|- ( 3 x. 3 ) = 9

Proof

Step	Hyp	Ref	Expression
1		df-3	|- 3 = ( 2 + 1 )
2	1	oveq2i	|- ( 3 x. 3 ) = ( 3 x. ( 2 + 1 ) )
3		3cn	|- 3 e. CC
4		2cn	|- 2 e. CC
5		ax-1cn	|- 1 e. CC
6	3 4 5	adddii	|- ( 3 x. ( 2 + 1 ) ) = ( ( 3 x. 2 ) + ( 3 x. 1 ) )
7		3t2e6	|- ( 3 x. 2 ) = 6
8		3t1e3	|- ( 3 x. 1 ) = 3
9	7 8	oveq12i	|- ( ( 3 x. 2 ) + ( 3 x. 1 ) ) = ( 6 + 3 )
10	6 9	eqtri	|- ( 3 x. ( 2 + 1 ) ) = ( 6 + 3 )
11		6p3e9	|- ( 6 + 3 ) = 9
12	10 11	eqtri	|- ( 3 x. ( 2 + 1 ) ) = 9
13	2 12	eqtri	|- ( 3 x. 3 ) = 9