Theorem 3t3e9 12425

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 12321	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7430	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12339	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12333	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11175	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11238	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12423	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12422	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7431	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2788	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12417	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2788	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2788	1 ⊢ (3 · 3) = 9

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11118   + caddc 11120   · cmul 11122  2c2 12312  3c3 12313  6c6 12316  9c9 12319

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-mulcl 11179  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-1rid 11187  ax-cnre 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325  df-8 12326  df-9 12327

This theorem is used by:  sq3  14254  3dvds  16413  3dvdsdec  16414  3dvds2dec  16415  9nprm  17196  11prm  17199  43prm  17206  83prm  17207  317prm  17210  1259lem2  17216  1259lem4  17218  1259prm  17220  2503lem2  17222  mcubic  27065  log2tlbnd  27163  log2ublem3  27166  log2ub  27167  bposlem9  27509  lgsdir2lem5  27546  ex-lcm  30882  hgt750lem  35105  hgt750lem2  35106  3lexlogpow2ineq2  42886  3lexlogpow5ineq5  42887  3cubeslem3l  43477  3cubeslem3r  43478  inductionexd  44941  fmtno5lem3  48367  fmtno4prmfac193  48385  fmtno4nprmfac193  48386  127prm  48411  2exp340mod341  48558  9fppr8  48562