Theorem 3t3e9 12337

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 12239	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7372	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12256	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12250	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11090	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11151	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12336	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12335	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7373	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2760	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12330	. . 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 1542  (class class class)co 7361  1c1 11033   + caddc 11035   · cmul 11037  2c2 12230  3c3 12231  6c6 12234  9c9 12237

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-1rid 11102  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244  df-9 12245

This theorem is referenced by:  sq3  14154  3dvds  16294  3dvdsdec  16295  3dvds2dec  16296  9nprm  17077  11prm  17079  43prm  17086  83prm  17087  317prm  17090  1259lem2  17096  1259lem4  17098  1259prm  17100  2503lem2  17102  mcubic  26827  log2tlbnd  26925  log2ublem3  26928  log2ub  26929  bposlem9  27272  lgsdir2lem5  27309  ex-lcm  30546  hgt750lem  34814  hgt750lem2  34815  3lexlogpow2ineq2  42515  3lexlogpow5ineq5  42516  3cubeslem3l  43135  3cubeslem3r  43136  inductionexd  44603  fmtno5lem3  48033  fmtno4prmfac193  48051  fmtno4nprmfac193  48052  127prm  48077  2exp340mod341  48224  9fppr8  48228