Theorem 3t2e6 11369

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 11285	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 11338	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 11351	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2780	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1630  (class class class)co 6811   + caddc 10129   · cmul 10131  2c2 11260  3c3 11261  6c6 11264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rrecex 10198  ax-cnre 10199

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-iota 6010  df-fv 6055  df-ov 6814  df-2 11269  df-3 11270  df-4 11271  df-5 11272  df-6 11273

This theorem is referenced by:  3t3e9  11370  8th4div3  11442  halfpm6th  11443  halfthird  11875  fac3  13259  bpoly3  14986  bpoly4  14987  sin01bnd  15112  3lcm2e6woprm  15528  3lcm2e6  15640  prmo3  15945  2exp6  15995  6nprm  16016  7prm  16017  17prm  16024  37prm  16028  83prm  16030  163prm  16032  317prm  16033  631prm  16034  1259lem3  16040  1259lem4  16041  1259lem5  16042  2503lem2  16045  4001lem1  16048  4001lem3  16050  4001prm  16052  sincos6thpi  24464  quart1  24780  log2ublem2  24871  log2ublem3  24872  log2ub  24873  basellem5  25008  basellem8  25011  cht3  25096  ppiublem1  25124  ppiub  25126  bclbnd  25202  bpos1  25205  bposlem8  25213  bposlem9  25214  2lgslem3d  25321  2lgsoddprmlem3d  25335  hgt750lem2  31037  problem4  31867  problem5  31868  pigt3  33713  lhe4.4ex1a  39028  stoweidlem13  40731  257prm  41981  127prm  42023  mod42tp1mod8  42027  6even  42128  2t6m3t4e0  42634  zlmodzxzequa  42793