Theorem 3t3e9 12355

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 12257	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7401	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12274	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12268	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11133	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11193	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12354	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12353	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7402	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2753	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12348	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2753	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2753	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   + caddc 11078   · cmul 11080  2c2 12248  3c3 12249  6c6 12252  9c9 12255

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263

This theorem is referenced by:  sq3  14170  3dvds  16308  3dvdsdec  16309  3dvds2dec  16310  9nprm  17090  11prm  17092  43prm  17099  83prm  17100  317prm  17103  1259lem2  17109  1259lem4  17111  1259prm  17113  2503lem2  17115  mcubic  26764  log2tlbnd  26862  log2ublem3  26865  log2ub  26866  bposlem9  27210  lgsdir2lem5  27247  ex-lcm  30394  hgt750lem  34649  hgt750lem2  34650  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  3cubeslem3l  42681  3cubeslem3r  42682  inductionexd  44151  fmtno5lem3  47560  fmtno4prmfac193  47578  fmtno4nprmfac193  47579  127prm  47604  2exp340mod341  47738  9fppr8  47742