Theorem 3t3e9 12386

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 12282	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7408	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12300	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12294	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11132	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11195	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12384	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12383	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7409	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2786	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12378	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2786	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2786	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1561  (class class class)co 7397  1c1 11075   + caddc 11077   · cmul 11079  2c2 12273  3c3 12274  6c6 12277  9c9 12280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-mulcl 11136  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-1rid 11144  ax-cnre 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6478  df-fv 6530  df-ov 7400  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-6 12285  df-7 12286  df-8 12287  df-9 12288

This theorem is referenced by:  sq3  14212  3dvds  16366  3dvdsdec  16367  3dvds2dec  16368  9nprm  17149  11prm  17152  43prm  17159  83prm  17160  317prm  17163  1259lem2  17169  1259lem4  17171  1259prm  17173  2503lem2  17175  mcubic  26913  log2tlbnd  27011  log2ublem3  27014  log2ub  27015  bposlem9  27357  lgsdir2lem5  27394  ex-lcm  30661  hgt750lem  34946  hgt750lem2  34947  3lexlogpow2ineq2  42677  3lexlogpow5ineq5  42678  3cubeslem3l  43268  3cubeslem3r  43269  inductionexd  44732  fmtno5lem3  48165  fmtno4prmfac193  48183  fmtno4nprmfac193  48184  127prm  48209  2exp340mod341  48356  9fppr8  48360