Theorem 3t2e6 12336

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 12256	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12309	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12322	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2760	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1542  (class class class)co 7361   + caddc 11035   · cmul 11037  2c2 12230  3c3 12231  6c6 12234

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 2709  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-1rid 11102  ax-cnre 11105

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 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242

This theorem is referenced by:  3t3e9  12337  8th4div3  12391  halfthird  12392  fac3  14236  bpoly3  16017  bpoly4  16018  sin01bnd  16146  3lcm2e6woprm  16578  3lcm2e6  16696  prmo3  17006  2exp6  17051  6nprm  17074  7prm  17075  17prm  17081  37prm  17085  83prm  17087  163prm  17089  317prm  17090  631prm  17091  1259lem3  17097  1259lem4  17098  1259lem5  17099  2503lem2  17102  4001lem1  17105  4001lem3  17107  4001prm  17109  sincos6thpi  26496  pigt3  26498  quart1  26836  log2ublem2  26927  log2ublem3  26928  log2ub  26929  basellem5  27065  basellem8  27068  cht3  27153  ppiublem1  27182  ppiub  27184  bclbnd  27260  bpos1  27263  bposlem8  27271  bposlem9  27272  2lgslem3d  27379  2lgsoddprmlem3d  27393  cos9thpiminplylem4  33948  cos9thpiminplylem5  33949  hgt750lem2  34815  problem4  35869  problem5  35870  3exp7  42509  3cubeslem3l  43135  3cubeslem3r  43136  lhe4.4ex1a  44777  stoweidlem13  46462  sin5tlem1  47340  sin5tlem4  47343  ceil5half3  47809  minusmodnep2tmod  47822  257prm  48039  127prm  48077  mod42tp1mod8  48080  ppivalnn4  48105  6even  48202  2exp340mod341  48224  2t6m3t4e0  48839  zlmodzxzequa  48987