Theorem 3t2e6 12342

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

Syntax hints:   = wceq 1542  (class class class)co 7367   + caddc 11041   · cmul 11043  2c2 12236  3c3 12237  6c6 12240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248

This theorem is referenced by:  3t3e9  12343  8th4div3  12397  halfthird  12398  fac3  14242  bpoly3  16023  bpoly4  16024  sin01bnd  16152  3lcm2e6woprm  16584  3lcm2e6  16702  prmo3  17012  2exp6  17057  6nprm  17080  7prm  17081  17prm  17087  37prm  17091  83prm  17093  163prm  17095  317prm  17096  631prm  17097  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem2  17108  4001lem1  17111  4001lem3  17113  4001prm  17115  sincos6thpi  26480  pigt3  26482  quart1  26820  log2ublem2  26911  log2ublem3  26912  log2ub  26913  basellem5  27048  basellem8  27051  cht3  27136  ppiublem1  27165  ppiub  27167  bclbnd  27243  bpos1  27246  bposlem8  27254  bposlem9  27255  2lgslem3d  27362  2lgsoddprmlem3d  27376  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  hgt750lem2  34796  problem4  35850  problem5  35851  3exp7  42492  3cubeslem3l  43118  3cubeslem3r  43119  lhe4.4ex1a  44756  stoweidlem13  46441  sin5tlem1  47321  sin5tlem4  47324  ceil5half3  47794  minusmodnep2tmod  47807  257prm  48024  127prm  48062  mod42tp1mod8  48065  ppivalnn4  48090  6even  48187  2exp340mod341  48209  2t6m3t4e0  48824  zlmodzxzequa  48972