Theorem 3t3e9 12433

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

Assertion

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

Proof of Theorem 3t3e9

Step	Hyp	Ref	Expression
1		df-3 12330	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7442	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12347	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12341	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11213	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11273	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12432	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12431	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7443	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2765	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12426	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2765	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2765	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158   · cmul 11160  2c2 12321  3c3 12322  6c6 12325  9c9 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336

This theorem is referenced by:  sq3  14237  3dvds  16368  3dvdsdec  16369  3dvds2dec  16370  9nprm  17150  11prm  17152  43prm  17159  83prm  17160  317prm  17163  1259lem2  17169  1259lem4  17171  1259prm  17173  2503lem2  17175  mcubic  26890  log2tlbnd  26988  log2ublem3  26991  log2ub  26992  bposlem9  27336  lgsdir2lem5  27373  ex-lcm  30477  hgt750lem  34666  hgt750lem2  34667  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  3cubeslem3l  42697  3cubeslem3r  42698  inductionexd  44168  fmtno5lem3  47542  fmtno4prmfac193  47560  fmtno4nprmfac193  47561  127prm  47586  2exp340mod341  47720  9fppr8  47724