Theorem 3t2e6 12304

Description: 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)

Assertion

Ref	Expression
3t2e6	⊢ (3 · 2) = 6

Proof of Theorem 3t2e6

Step	Hyp	Ref	Expression
1		3cn 12224	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12277	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12290	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2757	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1541  (class class class)co 7356   + caddc 11027   · cmul 11029  2c2 12198  3c3 12199  6c6 12202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-1rid 11094  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210

This theorem is referenced by:  3t3e9  12305  8th4div3  12359  halfthird  12360  fac3  14201  bpoly3  15979  bpoly4  15980  sin01bnd  16108  3lcm2e6woprm  16540  3lcm2e6  16657  prmo3  16967  2exp6  17012  6nprm  17035  7prm  17036  17prm  17042  37prm  17046  83prm  17048  163prm  17050  317prm  17051  631prm  17052  1259lem3  17058  1259lem4  17059  1259lem5  17060  2503lem2  17063  4001lem1  17066  4001lem3  17068  4001prm  17070  sincos6thpi  26479  pigt3  26481  quart1  26820  log2ublem2  26911  log2ublem3  26912  log2ub  26913  basellem5  27049  basellem8  27052  cht3  27137  ppiublem1  27167  ppiub  27169  bclbnd  27245  bpos1  27248  bposlem8  27256  bposlem9  27257  2lgslem3d  27364  2lgsoddprmlem3d  27378  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  hgt750lem2  34758  problem4  35811  problem5  35812  3exp7  42246  3cubeslem3l  42870  3cubeslem3r  42871  lhe4.4ex1a  44512  stoweidlem13  46199  ceil5half3  47528  minusmodnep2tmod  47541  257prm  47749  127prm  47787  mod42tp1mod8  47790  6even  47899  2exp340mod341  47921  2t6m3t4e0  48536  zlmodzxzequa  48684