Theorem 3t3e9 12510

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 12406	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7431	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12424	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12418	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11258	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11321	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12508	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12507	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7432	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2784	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12502	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2784	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2784	1 ⊢ (3 · 3) = 9

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420  1c1 11201   + caddc 11203   · cmul 11205  2c2 12397  3c3 12398  6c6 12401  9c9 12404

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-1rid 11270  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410  df-8 12411  df-9 12412

This theorem is used by:  sq3  14341  3dvds  16501  3dvdsdec  16502  3dvds2dec  16503  9nprm  17290  11prm  17293  43prm  17300  83prm  17301  317prm  17304  1259lem2  17310  1259lem4  17312  1259prm  17314  2503lem2  17316  mcubic  27175  log2tlbnd  27273  log2ublem3  27276  log2ub  27277  bposlem9  27619  lgsdir2lem5  27656  ex-lcm  31059  hgt750lem  35280  hgt750lem2  35281  3lexlogpow2ineq2  43109  3lexlogpow5ineq5  43110  3cubeslem3l  43696  3cubeslem3r  43697  inductionexd  45154  fmtno5lem3  48639  fmtno4prmfac193  48657  fmtno4nprmfac193  48658  127prm  48683  2exp340mod341  48830  9fppr8  48834