Theorem 3t3e9 12309

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 12211	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7369	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12228	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12222	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11086	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11146	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12308	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12307	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7370	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2759	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12302	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2759	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2759	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1541  (class class class)co 7358  1c1 11029   + caddc 11031   · cmul 11033  2c2 12202  3c3 12203  6c6 12206  9c9 12209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-1rid 11098  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217

This theorem is referenced by:  sq3  14123  3dvds  16260  3dvdsdec  16261  3dvds2dec  16262  9nprm  17042  11prm  17044  43prm  17051  83prm  17052  317prm  17055  1259lem2  17061  1259lem4  17063  1259prm  17065  2503lem2  17067  mcubic  26815  log2tlbnd  26913  log2ublem3  26916  log2ub  26917  bposlem9  27261  lgsdir2lem5  27298  ex-lcm  30535  hgt750lem  34810  hgt750lem2  34811  3lexlogpow2ineq2  42335  3lexlogpow5ineq5  42336  3cubeslem3l  42949  3cubeslem3r  42950  inductionexd  44417  fmtno5lem3  47822  fmtno4prmfac193  47840  fmtno4nprmfac193  47841  127prm  47866  2exp340mod341  48000  9fppr8  48004