Theorem 3t2e6 12429

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 12344	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12402	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12415	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2762	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1536  (class class class)co 7430   + caddc 11155   · cmul 11157  2c2 12318  3c3 12319  6c6 12322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-1rid 11222  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330

This theorem is referenced by:  3t3e9  12430  8th4div3  12483  halfpm6th  12484  halfthird  12873  fac3  14315  bpoly3  16090  bpoly4  16091  sin01bnd  16217  3lcm2e6woprm  16648  3lcm2e6  16765  prmo3  17074  2exp6  17120  6nprm  17143  7prm  17144  17prm  17150  37prm  17154  83prm  17156  163prm  17158  317prm  17159  631prm  17160  1259lem3  17166  1259lem4  17167  1259lem5  17168  2503lem2  17171  4001lem1  17174  4001lem3  17176  4001prm  17178  sincos6thpi  26572  pigt3  26574  quart1  26913  log2ublem2  27004  log2ublem3  27005  log2ub  27006  basellem5  27142  basellem8  27145  cht3  27230  ppiublem1  27260  ppiub  27262  bclbnd  27338  bpos1  27341  bposlem8  27349  bposlem9  27350  2lgslem3d  27457  2lgsoddprmlem3d  27471  hgt750lem2  34645  problem4  35652  problem5  35653  3exp7  42034  3cubeslem3l  42673  3cubeslem3r  42674  lhe4.4ex1a  44324  stoweidlem13  45968  ceil5half3  47279  minusmodnep2tmod  47292  257prm  47485  127prm  47523  mod42tp1mod8  47526  6even  47635  2exp340mod341  47657  2t6m3t4e0  48192  zlmodzxzequa  48341