Theorem 3t3e9 11792

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 11689	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7146	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 11706	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 11700	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 10584	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 10642	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 11791	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 11790	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7147	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2821	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 11785	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2821	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2821	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1538  (class class class)co 7135  1c1 10527   + caddc 10529   · cmul 10531  2c2 11680  3c3 11681  6c6 11684  9c9 11687

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695

This theorem is referenced by:  sq3  13557  3dvds  15672  3dvdsdec  15673  3dvds2dec  15674  9nprm  16438  11prm  16440  43prm  16447  83prm  16448  317prm  16451  1259lem2  16457  1259lem4  16459  1259prm  16461  2503lem2  16463  mcubic  25433  log2tlbnd  25531  log2ublem3  25534  log2ub  25535  bposlem9  25876  lgsdir2lem5  25913  ex-lcm  28243  hgt750lem  32032  hgt750lem2  32033  3lexlogpow5ineq2  39342  3cubeslem3l  39627  3cubeslem3r  39628  inductionexd  40858  fmtno5lem3  44072  fmtno4prmfac193  44090  fmtno4nprmfac193  44091  127prm  44116  2exp340mod341  44251  9fppr8  44255