Theorem 3t3e9 12305

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 12207	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7367	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12224	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12218	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11082	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11142	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12304	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12303	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7368	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2757	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12298	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2757	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2757	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   + caddc 11027   · cmul 11029  2c2 12198  3c3 12199  6c6 12202  9c9 12205

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 2706  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-1rid 11094  ax-cnre 11097

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 2713  df-cleq 2726  df-clel 2809  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210  df-7 12211  df-8 12212  df-9 12213

This theorem is referenced by:  sq3  14119  3dvds  16256  3dvdsdec  16257  3dvds2dec  16258  9nprm  17038  11prm  17040  43prm  17047  83prm  17048  317prm  17051  1259lem2  17057  1259lem4  17059  1259prm  17061  2503lem2  17063  mcubic  26811  log2tlbnd  26909  log2ublem3  26912  log2ub  26913  bposlem9  27257  lgsdir2lem5  27294  ex-lcm  30482  hgt750lem  34757  hgt750lem2  34758  3lexlogpow2ineq2  42252  3lexlogpow5ineq5  42253  3cubeslem3l  42870  3cubeslem3r  42871  inductionexd  44338  fmtno5lem3  47743  fmtno4prmfac193  47761  fmtno4nprmfac193  47762  127prm  47787  2exp340mod341  47921  9fppr8  47925