Theorem 3t3e9 12405

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 12302	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7414	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12319	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12313	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11185	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11245	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12404	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12403	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7415	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2758	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12398	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2758	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2758	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1540  (class class class)co 7403  1c1 11128   + caddc 11130   · cmul 11132  2c2 12293  3c3 12294  6c6 12297  9c9 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307  df-9 12308

This theorem is referenced by:  sq3  14214  3dvds  16348  3dvdsdec  16349  3dvds2dec  16350  9nprm  17130  11prm  17132  43prm  17139  83prm  17140  317prm  17143  1259lem2  17149  1259lem4  17151  1259prm  17153  2503lem2  17155  mcubic  26807  log2tlbnd  26905  log2ublem3  26908  log2ub  26909  bposlem9  27253  lgsdir2lem5  27290  ex-lcm  30385  hgt750lem  34629  hgt750lem2  34630  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  3cubeslem3l  42656  3cubeslem3r  42657  inductionexd  44126  fmtno5lem3  47517  fmtno4prmfac193  47535  fmtno4nprmfac193  47536  127prm  47561  2exp340mod341  47695  9fppr8  47699