Theorem 3t3e9 12431

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 12328	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7435	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12345	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12339	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11216	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11276	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12430	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12429	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7436	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2754	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12424	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2754	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2754	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1534  (class class class)co 7424  1c1 11159   + caddc 11161   · cmul 11163  2c2 12319  3c3 12320  6c6 12323  9c9 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-mulcl 11220  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-1rid 11228  ax-cnre 11231

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-iota 6506  df-fv 6562  df-ov 7427  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334

This theorem is referenced by:  sq3  14216  3dvds  16333  3dvdsdec  16334  3dvds2dec  16335  9nprm  17115  11prm  17117  43prm  17124  83prm  17125  317prm  17128  1259lem2  17134  1259lem4  17136  1259prm  17138  2503lem2  17140  mcubic  26875  log2tlbnd  26973  log2ublem3  26976  log2ub  26977  bposlem9  27321  lgsdir2lem5  27358  ex-lcm  30391  hgt750lem  34497  hgt750lem2  34498  3lexlogpow2ineq2  41758  3lexlogpow5ineq5  41759  3cubeslem3l  42343  3cubeslem3r  42344  inductionexd  43822  fmtno5lem3  47127  fmtno4prmfac193  47145  fmtno4nprmfac193  47146  127prm  47171  2exp340mod341  47305  9fppr8  47309