Theorem 3t2e6 12328

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 12243	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12301	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12314	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2759	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1541  (class class class)co 7362   + caddc 11063   · cmul 11065  2c2 12217  3c3 12218  6c6 12221

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-mulcl 11122  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-1rid 11130  ax-cnre 11133

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229

This theorem is referenced by:  3t3e9  12329  8th4div3  12382  halfpm6th  12383  halfthird  12770  fac3  14190  bpoly3  15952  bpoly4  15953  sin01bnd  16078  3lcm2e6woprm  16502  3lcm2e6  16618  prmo3  16924  2exp6  16970  6nprm  16993  7prm  16994  17prm  17000  37prm  17004  83prm  17006  163prm  17008  317prm  17009  631prm  17010  1259lem3  17016  1259lem4  17017  1259lem5  17018  2503lem2  17021  4001lem1  17024  4001lem3  17026  4001prm  17028  sincos6thpi  25909  pigt3  25911  quart1  26243  log2ublem2  26334  log2ublem3  26335  log2ub  26336  basellem5  26471  basellem8  26474  cht3  26559  ppiublem1  26587  ppiub  26589  bclbnd  26665  bpos1  26668  bposlem8  26676  bposlem9  26677  2lgslem3d  26784  2lgsoddprmlem3d  26798  hgt750lem2  33354  problem4  34343  problem5  34344  3exp7  40583  3cubeslem3l  41067  3cubeslem3r  41068  lhe4.4ex1a  42731  stoweidlem13  44374  257prm  45873  127prm  45911  mod42tp1mod8  45914  6even  46023  2exp340mod341  46045  2t6m3t4e0  46544  zlmodzxzequa  46697