Theorem 3t3e9 11884

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 11781	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7182	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 11798	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 11792	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 10674	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 10732	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 11883	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 11882	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7183	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2761	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 11877	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2761	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2761	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1542  (class class class)co 7171  1c1 10617   + caddc 10619   · cmul 10621  2c2 11772  3c3 11773  6c6 11776  9c9 11779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-resscn 10673  ax-1cn 10674  ax-icn 10675  ax-addcl 10676  ax-mulcl 10678  ax-mulcom 10680  ax-addass 10681  ax-mulass 10682  ax-distr 10683  ax-1rid 10686  ax-cnre 10689

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3400  df-un 3849  df-in 3851  df-ss 3861  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-iota 6298  df-fv 6348  df-ov 7174  df-2 11780  df-3 11781  df-4 11782  df-5 11783  df-6 11784  df-7 11785  df-8 11786  df-9 11787

This theorem is referenced by:  sq3  13654  3dvds  15777  3dvdsdec  15778  3dvds2dec  15779  9nprm  16550  11prm  16552  43prm  16559  83prm  16560  317prm  16563  1259lem2  16569  1259lem4  16571  1259prm  16573  2503lem2  16575  mcubic  25585  log2tlbnd  25683  log2ublem3  25686  log2ub  25687  bposlem9  26028  lgsdir2lem5  26065  ex-lcm  28395  hgt750lem  32201  hgt750lem2  32202  3lexlogpow2ineq2  39684  3lexlogpow5ineq5  39685  3cubeslem3l  40072  3cubeslem3r  40073  inductionexd  41303  fmtno5lem3  44533  fmtno4prmfac193  44551  fmtno4nprmfac193  44552  127prm  44577  2exp340mod341  44711  9fppr8  44715