Theorem 4t2e8 12310

Description: 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)

Assertion

Ref	Expression
4t2e8	⊢ (4 · 2) = 8

Proof of Theorem 4t2e8

Step	Hyp	Ref	Expression
1		4cn 12232	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12281	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12297	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2752	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1540  (class class class)co 7353   + caddc 11031   · cmul 11033  2c2 12202  4c4 12204  8c8 12208

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 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-1rid 11098  ax-cnre 11101

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216

This theorem is referenced by:  8th4div3  12363  4t3e12  12708  sq4e2t8  14125  cu2  14126  sqoddm1div8  14169  cos2bnd  16116  2exp7  17018  2exp8  17019  8nprm  17042  19prm  17048  139prm  17054  1259lem2  17062  1259lem3  17063  1259lem4  17064  1259lem5  17065  2503lem1  17067  2503lem2  17068  4001lem1  17071  4001lem2  17072  4001lem3  17073  4001lem4  17074  quart1lem  26782  quart1  26783  quartlem1  26784  log2tlbnd  26872  log2ub  26876  bpos1  27211  bposlem8  27219  lgsdir2lem2  27254  2lgslem3a  27324  2lgslem3b  27325  2lgslem3c  27326  2lgslem3d  27327  2lgsoddprmlem2  27337  2lgsoddprmlem3c  27340  2lgsoddprmlem3d  27341  chebbnd1lem2  27398  chebbnd1lem3  27399  pntlemr  27530  ex-exp  30413  420gcd8e4  41999  420lcm8e840  42004  lcmineqlem23  42044  3lexlogpow2ineq2  42052  sum9cubes  42665  fmtno4prmfac  47576  139prmALT  47600  mod42tp1mod8  47606  3exp4mod41  47620  41prothprm  47623  8even  47717  2exp340mod341  47737  8exp8mod9  47740  pgnbgreunbgrlem4  48123