Theorem 3t3e9 12378

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 12275	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7419	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12292	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12286	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11167	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11225	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12377	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12376	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7420	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2760	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12371	. . 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 7408  1c1 11110   + caddc 11112   · cmul 11114  2c2 12266  3c3 12267  6c6 12270  9c9 12273

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 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-mulcl 11171  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-1rid 11179  ax-cnre 11182

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281

This theorem is referenced by:  sq3  14161  3dvds  16273  3dvdsdec  16274  3dvds2dec  16275  9nprm  17045  11prm  17047  43prm  17054  83prm  17055  317prm  17058  1259lem2  17064  1259lem4  17066  1259prm  17068  2503lem2  17070  mcubic  26349  log2tlbnd  26447  log2ublem3  26450  log2ub  26451  bposlem9  26792  lgsdir2lem5  26829  ex-lcm  29708  hgt750lem  33658  hgt750lem2  33659  3lexlogpow2ineq2  40919  3lexlogpow5ineq5  40920  3cubeslem3l  41414  3cubeslem3r  41415  inductionexd  42896  fmtno5lem3  46213  fmtno4prmfac193  46231  fmtno4nprmfac193  46232  127prm  46257  2exp340mod341  46391  9fppr8  46395