Theorem 3t2e6 12308

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 12228	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12281	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12294	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2759	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1541  (class class class)co 7358   + caddc 11031   · cmul 11033  2c2 12202  3c3 12203  6c6 12206

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 2708  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-1rid 11098  ax-cnre 11101

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 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214

This theorem is referenced by:  3t3e9  12309  8th4div3  12363  halfthird  12364  fac3  14205  bpoly3  15983  bpoly4  15984  sin01bnd  16112  3lcm2e6woprm  16544  3lcm2e6  16661  prmo3  16971  2exp6  17016  6nprm  17039  7prm  17040  17prm  17046  37prm  17050  83prm  17052  163prm  17054  317prm  17055  631prm  17056  1259lem3  17062  1259lem4  17063  1259lem5  17064  2503lem2  17067  4001lem1  17070  4001lem3  17072  4001prm  17074  sincos6thpi  26483  pigt3  26485  quart1  26824  log2ublem2  26915  log2ublem3  26916  log2ub  26917  basellem5  27053  basellem8  27056  cht3  27141  ppiublem1  27171  ppiub  27173  bclbnd  27249  bpos1  27252  bposlem8  27260  bposlem9  27261  2lgslem3d  27368  2lgsoddprmlem3d  27382  cos9thpiminplylem4  33944  cos9thpiminplylem5  33945  hgt750lem2  34811  problem4  35864  problem5  35865  3exp7  42329  3cubeslem3l  42949  3cubeslem3r  42950  lhe4.4ex1a  44591  stoweidlem13  46278  ceil5half3  47607  minusmodnep2tmod  47620  257prm  47828  127prm  47866  mod42tp1mod8  47869  6even  47978  2exp340mod341  48000  2t6m3t4e0  48615  zlmodzxzequa  48763