Theorem 3t2e6 12347

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 12267	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12320	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12333	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2752	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1540  (class class class)co 7387   + caddc 11071   · cmul 11073  2c2 12241  3c3 12242  6c6 12245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253

This theorem is referenced by:  3t3e9  12348  8th4div3  12402  halfthird  12403  fac3  14245  bpoly3  16024  bpoly4  16025  sin01bnd  16153  3lcm2e6woprm  16585  3lcm2e6  16702  prmo3  17012  2exp6  17057  6nprm  17080  7prm  17081  17prm  17087  37prm  17091  83prm  17093  163prm  17095  317prm  17096  631prm  17097  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem2  17108  4001lem1  17111  4001lem3  17113  4001prm  17115  sincos6thpi  26425  pigt3  26427  quart1  26766  log2ublem2  26857  log2ublem3  26858  log2ub  26859  basellem5  26995  basellem8  26998  cht3  27083  ppiublem1  27113  ppiub  27115  bclbnd  27191  bpos1  27194  bposlem8  27202  bposlem9  27203  2lgslem3d  27310  2lgsoddprmlem3d  27324  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  hgt750lem2  34643  problem4  35655  problem5  35656  3exp7  42041  3cubeslem3l  42674  3cubeslem3r  42675  lhe4.4ex1a  44318  stoweidlem13  46011  ceil5half3  47341  minusmodnep2tmod  47354  257prm  47562  127prm  47600  mod42tp1mod8  47603  6even  47712  2exp340mod341  47734  2t6m3t4e0  48336  zlmodzxzequa  48485