Theorem 3t2e6 12382

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

Syntax hints:   = wceq 1541  (class class class)co 7411   + caddc 11115   · cmul 11117  2c2 12271  3c3 12272  6c6 12275

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-mulcl 11174  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-1rid 11182  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283

This theorem is referenced by:  3t3e9  12383  8th4div3  12436  halfpm6th  12437  halfthird  12824  fac3  14244  bpoly3  16006  bpoly4  16007  sin01bnd  16132  3lcm2e6woprm  16556  3lcm2e6  16672  prmo3  16978  2exp6  17024  6nprm  17047  7prm  17048  17prm  17054  37prm  17058  83prm  17060  163prm  17062  317prm  17063  631prm  17064  1259lem3  17070  1259lem4  17071  1259lem5  17072  2503lem2  17075  4001lem1  17078  4001lem3  17080  4001prm  17082  sincos6thpi  26249  pigt3  26251  quart1  26585  log2ublem2  26676  log2ublem3  26677  log2ub  26678  basellem5  26813  basellem8  26816  cht3  26901  ppiublem1  26929  ppiub  26931  bclbnd  27007  bpos1  27010  bposlem8  27018  bposlem9  27019  2lgslem3d  27126  2lgsoddprmlem3d  27140  hgt750lem2  33950  problem4  34939  problem5  34940  3exp7  41224  3cubeslem3l  41726  3cubeslem3r  41727  lhe4.4ex1a  43390  stoweidlem13  45028  257prm  46528  127prm  46566  mod42tp1mod8  46569  6even  46678  2exp340mod341  46700  2t6m3t4e0  47113  zlmodzxzequa  47265