Theorem 3t3e9 12375

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 12272	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7416	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12289	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12283	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11164	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11222	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12374	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12373	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7417	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2760	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12368	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2760	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2760	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1541  (class class class)co 7405  1c1 11107   + caddc 11109   · cmul 11111  2c2 12263  3c3 12264  6c6 12267  9c9 12270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-mulcl 11168  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-1rid 11176  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278

This theorem is referenced by:  sq3  14158  3dvds  16270  3dvdsdec  16271  3dvds2dec  16272  9nprm  17042  11prm  17044  43prm  17051  83prm  17052  317prm  17055  1259lem2  17061  1259lem4  17063  1259prm  17065  2503lem2  17067  mcubic  26341  log2tlbnd  26439  log2ublem3  26442  log2ub  26443  bposlem9  26784  lgsdir2lem5  26821  ex-lcm  29700  hgt750lem  33651  hgt750lem2  33652  3lexlogpow2ineq2  40912  3lexlogpow5ineq5  40913  3cubeslem3l  41409  3cubeslem3r  41410  inductionexd  42891  fmtno5lem3  46209  fmtno4prmfac193  46227  fmtno4nprmfac193  46228  127prm  46253  2exp340mod341  46387  9fppr8  46391