Theorem 3t2e6 12139

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 12054	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12112	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12125	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2768	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1542  (class class class)co 7271   + caddc 10875   · cmul 10877  2c2 12028  3c3 12029  6c6 12032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-mulcl 10934  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-1rid 10942  ax-cnre 10945

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-iota 6390  df-fv 6440  df-ov 7274  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040

This theorem is referenced by:  3t3e9  12140  8th4div3  12193  halfpm6th  12194  halfthird  12579  fac3  13992  bpoly3  15766  bpoly4  15767  sin01bnd  15892  3lcm2e6woprm  16318  3lcm2e6  16434  prmo3  16740  2exp6  16786  6nprm  16809  7prm  16810  17prm  16816  37prm  16820  83prm  16822  163prm  16824  317prm  16825  631prm  16826  1259lem3  16832  1259lem4  16833  1259lem5  16834  2503lem2  16837  4001lem1  16840  4001lem3  16842  4001prm  16844  sincos6thpi  25670  pigt3  25672  quart1  26004  log2ublem2  26095  log2ublem3  26096  log2ub  26097  basellem5  26232  basellem8  26235  cht3  26320  ppiublem1  26348  ppiub  26350  bclbnd  26426  bpos1  26429  bposlem8  26437  bposlem9  26438  2lgslem3d  26545  2lgsoddprmlem3d  26559  hgt750lem2  32628  problem4  33622  problem5  33623  3exp7  40058  3cubeslem3l  40505  3cubeslem3r  40506  lhe4.4ex1a  41917  stoweidlem13  43525  257prm  44982  127prm  45020  mod42tp1mod8  45023  6even  45132  2exp340mod341  45154  2t6m3t4e0  45653  zlmodzxzequa  45806