Theorem 3t3e9 12379

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 12276	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7420	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12293	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12287	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11168	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11226	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12378	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12377	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7421	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2761	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12372	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2761	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2761	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1542  (class class class)co 7409  1c1 11111   + caddc 11113   · cmul 11115  2c2 12267  3c3 12268  6c6 12271  9c9 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-1rid 11180  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282

This theorem is referenced by:  sq3  14162  3dvds  16274  3dvdsdec  16275  3dvds2dec  16276  9nprm  17046  11prm  17048  43prm  17055  83prm  17056  317prm  17059  1259lem2  17065  1259lem4  17067  1259prm  17069  2503lem2  17071  mcubic  26352  log2tlbnd  26450  log2ublem3  26453  log2ub  26454  bposlem9  26795  lgsdir2lem5  26832  ex-lcm  29711  hgt750lem  33663  hgt750lem2  33664  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  3cubeslem3l  41424  3cubeslem3r  41425  inductionexd  42906  fmtno5lem3  46223  fmtno4prmfac193  46241  fmtno4nprmfac193  46242  127prm  46267  2exp340mod341  46401  9fppr8  46405