Theorem 3t3e9 12408

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 12304	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7422	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12322	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12316	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11158	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11221	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12406	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12405	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7423	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2792	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12400	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2792	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2792	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11101   + caddc 11103   · cmul 11105  2c2 12295  3c3 12296  6c6 12299  9c9 12302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-mulcl 11162  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-1rid 11170  ax-cnre 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309  df-9 12310

This theorem is referenced by:  sq3  14234  3dvds  16389  3dvdsdec  16390  3dvds2dec  16391  9nprm  17172  11prm  17175  43prm  17182  83prm  17183  317prm  17186  1259lem2  17192  1259lem4  17194  1259prm  17196  2503lem2  17198  mcubic  26978  log2tlbnd  27076  log2ublem3  27079  log2ub  27080  bposlem9  27422  lgsdir2lem5  27459  ex-lcm  30750  hgt750lem  34983  hgt750lem2  34984  3lexlogpow2ineq2  42750  3lexlogpow5ineq5  42751  3cubeslem3l  43343  3cubeslem3r  43344  inductionexd  44807  fmtno5lem3  48230  fmtno4prmfac193  48248  fmtno4nprmfac193  48249  127prm  48274  2exp340mod341  48421  9fppr8  48425