Theorem 3t3e9 12403

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 12299	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7421	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12317	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12311	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11153	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11216	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12401	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12400	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7422	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2786	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12395	. . 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 1570  (class class class)co 7410  1c1 11096   + caddc 11098   · cmul 11100  2c2 12290  3c3 12291  6c6 12294  9c9 12297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-1rid 11165  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304  df-9 12305

This theorem is referenced by:  sq3  14230  3dvds  16384  3dvdsdec  16385  3dvds2dec  16386  9nprm  17167  11prm  17170  43prm  17177  83prm  17178  317prm  17181  1259lem2  17187  1259lem4  17189  1259prm  17191  2503lem2  17193  mcubic  27012  log2tlbnd  27110  log2ublem3  27113  log2ub  27114  bposlem9  27456  lgsdir2lem5  27493  ex-lcm  30809  hgt750lem  35038  hgt750lem2  35039  3lexlogpow2ineq2  42846  3lexlogpow5ineq5  42847  3cubeslem3l  43437  3cubeslem3r  43438  inductionexd  44901  fmtno5lem3  48327  fmtno4prmfac193  48345  fmtno4nprmfac193  48346  127prm  48371  2exp340mod341  48518  9fppr8  48522