Theorem 3t3e9 12348

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 12250	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7398	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12267	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12261	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11126	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11186	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12347	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12346	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7399	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2752	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12341	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2752	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2752	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071   · cmul 11073  2c2 12241  3c3 12242  6c6 12245  9c9 12248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256

This theorem is referenced by:  sq3  14163  3dvds  16301  3dvdsdec  16302  3dvds2dec  16303  9nprm  17083  11prm  17085  43prm  17092  83prm  17093  317prm  17096  1259lem2  17102  1259lem4  17104  1259prm  17106  2503lem2  17108  mcubic  26757  log2tlbnd  26855  log2ublem3  26858  log2ub  26859  bposlem9  27203  lgsdir2lem5  27240  ex-lcm  30387  hgt750lem  34642  hgt750lem2  34643  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  3cubeslem3l  42674  3cubeslem3r  42675  inductionexd  44144  fmtno5lem3  47556  fmtno4prmfac193  47574  fmtno4nprmfac193  47575  127prm  47600  2exp340mod341  47734  9fppr8  47738