Theorem 3t3e9 12290

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 12192	. . 3 ⊢ 3 = (2 + 1)
2	1	oveq2i 7360	. 2 ⊢ (3 · 3) = (3 · (2 + 1))
3		3cn 12209	. . . . 5 ⊢ 3 ∈ ℂ
4		2cn 12203	. . . . 5 ⊢ 2 ∈ ℂ
5		ax-1cn 11067	. . . . 5 ⊢ 1 ∈ ℂ
6	3, 4, 5	adddii 11127	. . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7		3t2e6 12289	. . . . 5 ⊢ (3 · 2) = 6
8		3t1e3 12288	. . . . 5 ⊢ (3 · 1) = 3
9	7, 8	oveq12i 7361	. . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3)
10	6, 9	eqtri 2752	. . 3 ⊢ (3 · (2 + 1)) = (6 + 3)
11		6p3e9 12283	. . 3 ⊢ (6 + 3) = 9
12	10, 11	eqtri 2752	. 2 ⊢ (3 · (2 + 1)) = 9
13	2, 12	eqtri 2752	1 ⊢ (3 · 3) = 9

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012   · cmul 11014  2c2 12183  3c3 12184  6c6 12187  9c9 12190

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-1rid 11079  ax-cnre 11082

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196  df-8 12197  df-9 12198

This theorem is referenced by:  sq3  14105  3dvds  16242  3dvdsdec  16243  3dvds2dec  16244  9nprm  17024  11prm  17026  43prm  17033  83prm  17034  317prm  17037  1259lem2  17043  1259lem4  17045  1259prm  17047  2503lem2  17049  mcubic  26755  log2tlbnd  26853  log2ublem3  26856  log2ub  26857  bposlem9  27201  lgsdir2lem5  27238  ex-lcm  30402  hgt750lem  34625  hgt750lem2  34626  3lexlogpow2ineq2  42042  3lexlogpow5ineq5  42043  3cubeslem3l  42669  3cubeslem3r  42670  inductionexd  44138  fmtno5lem3  47549  fmtno4prmfac193  47567  fmtno4nprmfac193  47568  127prm  47593  2exp340mod341  47727  9fppr8  47731