Theorem 3t2e6 12383

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 12299	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12356	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12369	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2785	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1560  (class class class)co 7396   + caddc 11076   · cmul 11078  2c2 12272  3c3 12273  6c6 12276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-mulcl 11135  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-1rid 11143  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284

This theorem is referenced by:  2t3e6  12384  3t3e9  12385  8th4div3  12441  halfthird  12442  fac3  14293  bpoly3  16088  bpoly4  16089  sin01bnd  16217  3lcm2e6woprm  16649  3lcm2e6  16767  prmo3  17077  2exp6  17122  6nprm  17145  7prm  17146  17prm  17153  37prm  17157  83prm  17159  163prm  17161  317prm  17162  631prm  17163  1259lem3  17169  1259lem4  17170  1259lem5  17171  2503lem2  17174  4001lem1  17177  4001lem3  17179  4001prm  17181  sincos6thpi  26581  pigt3  26583  quart1  26921  log2ublem2  27012  log2ublem3  27013  log2ub  27014  basellem5  27149  basellem8  27152  ppiublem1  27266  ppiub  27268  bclbnd  27344  bpos1  27347  bposlem8  27355  bposlem9  27356  2lgslem3d  27463  2lgsoddprmlem3d  27477  cos9thpiminplylem4  34082  cos9thpiminplylem5  34083  hgt750lem2  34946  problem4  36018  problem5  36019  3exp7  42670  3cubeslem3l  43267  3cubeslem3r  43268  lhe4.4ex1a  44905  stoweidlem13  46587  sin5tlem1  47467  sin5tlem4  47470  ceil5half3  47940  minusmodnep2tmod  47953  257prm  48170  127prm  48208  ppivalnn4  48236  6even  48333  2exp340mod341  48355  2t6m3t4e0  48970  zlmodzxzequa  49118