Theorem 3t2e6 11548

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 11456	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 11521	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 11534	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2802	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1601  (class class class)co 6922   + caddc 10275   · cmul 10277  2c2 11430  3c3 11431  6c6 11434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-mulcl 10334  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-1rid 10342  ax-cnre 10345

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442

This theorem is referenced by:  3t3e9  11549  8th4div3  11602  halfpm6th  11603  halfthird  11990  fac3  13385  bpoly3  15191  bpoly4  15192  sin01bnd  15317  3lcm2e6woprm  15734  3lcm2e6  15844  prmo3  16149  2exp6  16194  6nprm  16215  7prm  16216  17prm  16222  37prm  16226  83prm  16228  163prm  16230  317prm  16231  631prm  16232  1259lem3  16238  1259lem4  16239  1259lem5  16240  2503lem2  16243  4001lem1  16246  4001lem3  16248  4001prm  16250  sincos6thpi  24705  quart1  25034  log2ublem2  25126  log2ublem3  25127  log2ub  25128  basellem5  25263  basellem8  25266  cht3  25351  ppiublem1  25379  ppiub  25381  bclbnd  25457  bpos1  25460  bposlem8  25468  bposlem9  25469  2lgslem3d  25576  2lgsoddprmlem3d  25590  hgt750lem2  31332  problem4  32159  problem5  32160  pigt3  34027  lhe4.4ex1a  39484  stoweidlem13  41157  257prm  42494  127prm  42536  mod42tp1mod8  42540  6even  42645  2t6m3t4e0  43141  zlmodzxzequa  43300