Theorem 3t3e9 12278

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 12180	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7351	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12197	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12191	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11055	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11115	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12277	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12276	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7352	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2752	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12271	. . 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 7340  1c1 10998   + caddc 11000   · cmul 11002  2c2 12171  3c3 12172  6c6 12175  9c9 12178

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 11054  ax-1cn 11055  ax-icn 11056  ax-addcl 11057  ax-mulcl 11059  ax-mulcom 11061  ax-addass 11062  ax-mulass 11063  ax-distr 11064  ax-1rid 11067  ax-cnre 11070

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 3393  df-v 3435  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-iota 6432  df-fv 6484  df-ov 7343  df-2 12179  df-3 12180  df-4 12181  df-5 12182  df-6 12183  df-7 12184  df-8 12185  df-9 12186

This theorem is referenced by:  sq3  14093  3dvds  16229  3dvdsdec  16230  3dvds2dec  16231  9nprm  17011  11prm  17013  43prm  17020  83prm  17021  317prm  17024  1259lem2  17030  1259lem4  17032  1259prm  17034  2503lem2  17036  mcubic  26738  log2tlbnd  26836  log2ublem3  26839  log2ub  26840  bposlem9  27184  lgsdir2lem5  27221  ex-lcm  30389  hgt750lem  34632  hgt750lem2  34633  3lexlogpow2ineq2  42049  3lexlogpow5ineq5  42050  3cubeslem3l  42676  3cubeslem3r  42677  inductionexd  44145  fmtno5lem3  47553  fmtno4prmfac193  47571  fmtno4nprmfac193  47572  127prm  47597  2exp340mod341  47731  9fppr8  47735