Theorem 3t2e6 12404

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 12319	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12377	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12390	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2758	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1540  (class class class)co 7403   + caddc 11130   · cmul 11132  2c2 12293  3c3 12294  6c6 12297

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305

This theorem is referenced by:  3t3e9  12405  8th4div3  12459  halfthird  12460  fac3  14296  bpoly3  16072  bpoly4  16073  sin01bnd  16201  3lcm2e6woprm  16632  3lcm2e6  16749  prmo3  17059  2exp6  17104  6nprm  17127  7prm  17128  17prm  17134  37prm  17138  83prm  17140  163prm  17142  317prm  17143  631prm  17144  1259lem3  17150  1259lem4  17151  1259lem5  17152  2503lem2  17155  4001lem1  17158  4001lem3  17160  4001prm  17162  sincos6thpi  26475  pigt3  26477  quart1  26816  log2ublem2  26907  log2ublem3  26908  log2ub  26909  basellem5  27045  basellem8  27048  cht3  27133  ppiublem1  27163  ppiub  27165  bclbnd  27241  bpos1  27244  bposlem8  27252  bposlem9  27253  2lgslem3d  27360  2lgsoddprmlem3d  27374  cos9thpiminplylem4  33765  cos9thpiminplylem5  33766  hgt750lem2  34630  problem4  35636  problem5  35637  3exp7  42012  3cubeslem3l  42656  3cubeslem3r  42657  lhe4.4ex1a  44301  stoweidlem13  45990  ceil5half3  47317  minusmodnep2tmod  47330  257prm  47523  127prm  47561  mod42tp1mod8  47564  6even  47673  2exp340mod341  47695  2t6m3t4e0  48271  zlmodzxzequa  48420