Theorem 3t2e6 12378

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 12293	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12351	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12364	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2761	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1542  (class class class)co 7409   + caddc 11113   · cmul 11115  2c2 12267  3c3 12268  6c6 12271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-1rid 11180  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279

This theorem is referenced by:  3t3e9  12379  8th4div3  12432  halfpm6th  12433  halfthird  12820  fac3  14240  bpoly3  16002  bpoly4  16003  sin01bnd  16128  3lcm2e6woprm  16552  3lcm2e6  16668  prmo3  16974  2exp6  17020  6nprm  17043  7prm  17044  17prm  17050  37prm  17054  83prm  17056  163prm  17058  317prm  17059  631prm  17060  1259lem3  17066  1259lem4  17067  1259lem5  17068  2503lem2  17071  4001lem1  17074  4001lem3  17076  4001prm  17078  sincos6thpi  26025  pigt3  26027  quart1  26361  log2ublem2  26452  log2ublem3  26453  log2ub  26454  basellem5  26589  basellem8  26592  cht3  26677  ppiublem1  26705  ppiub  26707  bclbnd  26783  bpos1  26786  bposlem8  26794  bposlem9  26795  2lgslem3d  26902  2lgsoddprmlem3d  26916  hgt750lem2  33664  problem4  34653  problem5  34654  3exp7  40918  3cubeslem3l  41424  3cubeslem3r  41425  lhe4.4ex1a  43088  stoweidlem13  44729  257prm  46229  127prm  46267  mod42tp1mod8  46270  6even  46379  2exp340mod341  46401  2t6m3t4e0  47024  zlmodzxzequa  47177