Theorem 3t2e6 11791

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 11706	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 11764	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 11777	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2821	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1538  (class class class)co 7135   + caddc 10529   · cmul 10531  2c2 11680  3c3 11681  6c6 11684

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692

This theorem is referenced by:  3t3e9  11792  8th4div3  11845  halfpm6th  11846  halfthird  12229  fac3  13636  bpoly3  15404  bpoly4  15405  sin01bnd  15530  3lcm2e6woprm  15949  3lcm2e6  16062  prmo3  16367  2exp6  16413  6nprm  16435  7prm  16436  17prm  16442  37prm  16446  83prm  16448  163prm  16450  317prm  16451  631prm  16452  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem2  16463  4001lem1  16466  4001lem3  16468  4001prm  16470  sincos6thpi  25108  pigt3  25110  quart1  25442  log2ublem2  25533  log2ublem3  25534  log2ub  25535  basellem5  25670  basellem8  25673  cht3  25758  ppiublem1  25786  ppiub  25788  bclbnd  25864  bpos1  25867  bposlem8  25875  bposlem9  25876  2lgslem3d  25983  2lgsoddprmlem3d  25997  hgt750lem2  32033  problem4  33024  problem5  33025  3cubeslem3l  39627  3cubeslem3r  39628  lhe4.4ex1a  41033  stoweidlem13  42655  257prm  44078  127prm  44116  mod42tp1mod8  44120  6even  44229  2exp340mod341  44251  2t6m3t4e0  44750  zlmodzxzequa  44905