Theorem 3t2e6 12414

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 12329	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12387	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12400	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2755	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1533  (class class class)co 7424   + caddc 11147   · cmul 11149  2c2 12303  3c3 12304  6c6 12307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-mulcl 11206  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-1rid 11214  ax-cnre 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rex 3067  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-iota 6503  df-fv 6559  df-ov 7427  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315

This theorem is referenced by:  3t3e9  12415  8th4div3  12468  halfpm6th  12469  halfthird  12856  fac3  14277  bpoly3  16040  bpoly4  16041  sin01bnd  16167  3lcm2e6woprm  16591  3lcm2e6  16709  prmo3  17015  2exp6  17061  6nprm  17084  7prm  17085  17prm  17091  37prm  17095  83prm  17097  163prm  17099  317prm  17100  631prm  17101  1259lem3  17107  1259lem4  17108  1259lem5  17109  2503lem2  17112  4001lem1  17115  4001lem3  17117  4001prm  17119  sincos6thpi  26468  pigt3  26470  quart1  26806  log2ublem2  26897  log2ublem3  26898  log2ub  26899  basellem5  27035  basellem8  27038  cht3  27123  ppiublem1  27153  ppiub  27155  bclbnd  27231  bpos1  27234  bposlem8  27242  bposlem9  27243  2lgslem3d  27350  2lgsoddprmlem3d  27364  hgt750lem2  34289  problem4  35277  problem5  35278  3exp7  41528  3cubeslem3l  42109  3cubeslem3r  42110  lhe4.4ex1a  43769  stoweidlem13  45403  257prm  46903  127prm  46941  mod42tp1mod8  46944  6even  47053  2exp340mod341  47075  2t6m3t4e0  47463  zlmodzxzequa  47615