Theorem 3t3e9 12523

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 12419	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7441	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12437	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12431	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11271	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11334	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12521	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12520	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7442	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2786	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12515	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2786	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2786	1 ⊢ (3 · 3) = 9

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7430  1c1 11214   + caddc 11216   · cmul 11218  2c2 12410  3c3 12411  6c6 12414  9c9 12417

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-mulcl 11275  ax-mulcom 11277  ax-addass 11278  ax-mulass 11279  ax-distr 11280  ax-1rid 11283  ax-cnre 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555  df-ov 7433  df-2 12418  df-3 12419  df-4 12420  df-5 12421  df-6 12422  df-7 12423  df-8 12424  df-9 12425

This theorem is used by:  sq3  14354  3dvds  16516  3dvdsdec  16517  3dvds2dec  16518  9nprm  17305  11prm  17308  43prm  17315  83prm  17316  317prm  17319  1259lem2  17325  1259lem4  17327  1259prm  17329  2503lem2  17331  mcubic  27190  log2tlbnd  27288  log2ublem3  27291  log2ub  27292  bposlem9  27634  lgsdir2lem5  27671  ex-lcm  31074  hgt750lem  35336  hgt750lem2  35337  3lexlogpow2ineq2  43252  3lexlogpow5ineq5  43253  3cubeslem3l  43839  3cubeslem3r  43840  inductionexd  45298  fmtno5lem3  48782  fmtno4prmfac193  48800  fmtno4nprmfac193  48801  127prm  48826  2exp340mod341  48973  9fppr8  48977