Theorem 3t2e6 12401

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 12317	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12374	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12387	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2786	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1570  (class class class)co 7410   + caddc 11098   · cmul 11100  2c2 12290  3c3 12291  6c6 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-1rid 11165  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302

This theorem is referenced by:  2t3e6  12402  3t3e9  12403  bpoly3  16107  bpoly4  16108  sin01bnd  16236  3lcm2e6woprm  16668  3lcm2e6  16786  6nprm  17164  7prm  17165  17prm  17172  37prm  17176  83prm  17178  163prm  17180  317prm  17181  631prm  17182  1259lem4  17189  2503lem2  17193  4001lem1  17196  4001lem3  17198  4001prm  17200  sincos6thpi  26681  pigt3  26683  log2ublem3  27113  log2ub  27114  basellem5  27249  ppiublem1  27366  bclbnd  27444  bpos1  27447  bposlem9  27456  2lgslem3d  27563  cos9thpiminplylem4  34175  cos9thpiminplylem5  34176  hgt750lem2  35039  problem4  36160  problem5  36161  3cubeslem3l  43437  3cubeslem3r  43438  lhe4.4ex1a  45059  stoweidlem13  46747  sin5tlem1  47630  sin5tlem4  47633  ceil5half3  48103  minusmodnep2tmod  48116  257prm  48333  127prm  48371  ppivalnn4  48399  6even  48496  2exp340mod341  48518  2t6m3t4e0  49148  zlmodzxzequa  49296