Theorem 3t2e6 12432

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 12347	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12405	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12418	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2765	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1540  (class class class)co 7431   + caddc 11158   · cmul 11160  2c2 12321  3c3 12322  6c6 12325

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333

This theorem is referenced by:  3t3e9  12433  8th4div3  12486  halfpm6th  12487  halfthird  12876  fac3  14319  bpoly3  16094  bpoly4  16095  sin01bnd  16221  3lcm2e6woprm  16652  3lcm2e6  16769  prmo3  17079  2exp6  17124  6nprm  17147  7prm  17148  17prm  17154  37prm  17158  83prm  17160  163prm  17162  317prm  17163  631prm  17164  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem2  17175  4001lem1  17178  4001lem3  17180  4001prm  17182  sincos6thpi  26558  pigt3  26560  quart1  26899  log2ublem2  26990  log2ublem3  26991  log2ub  26992  basellem5  27128  basellem8  27131  cht3  27216  ppiublem1  27246  ppiub  27248  bclbnd  27324  bpos1  27327  bposlem8  27335  bposlem9  27336  2lgslem3d  27443  2lgsoddprmlem3d  27457  hgt750lem2  34667  problem4  35673  problem5  35674  3exp7  42054  3cubeslem3l  42697  3cubeslem3r  42698  lhe4.4ex1a  44348  stoweidlem13  46028  ceil5half3  47342  minusmodnep2tmod  47355  257prm  47548  127prm  47586  mod42tp1mod8  47589  6even  47698  2exp340mod341  47720  2t6m3t4e0  48264  zlmodzxzequa  48413