Theorem 4t2e8 12283

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 12205	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12254	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12270	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2754	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1541  (class class class)co 7341   + caddc 11004   · cmul 11006  2c2 12175  4c4 12177  8c8 12181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-mulcl 11063  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-1rid 11071  ax-cnre 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-ov 7344  df-2 12183  df-3 12184  df-4 12185  df-5 12186  df-6 12187  df-7 12188  df-8 12189

This theorem is referenced by:  8th4div3  12336  4t3e12  12681  sq4e2t8  14101  cu2  14102  sqoddm1div8  14145  cos2bnd  16092  2exp7  16994  2exp8  16995  8nprm  17018  19prm  17024  139prm  17030  1259lem2  17038  1259lem3  17039  1259lem4  17040  1259lem5  17041  2503lem1  17043  2503lem2  17044  4001lem1  17047  4001lem2  17048  4001lem3  17049  4001lem4  17050  quart1lem  26787  quart1  26788  quartlem1  26789  log2tlbnd  26877  log2ub  26881  bpos1  27216  bposlem8  27224  lgsdir2lem2  27259  2lgslem3a  27329  2lgslem3b  27330  2lgslem3c  27331  2lgslem3d  27332  2lgsoddprmlem2  27342  2lgsoddprmlem3c  27345  2lgsoddprmlem3d  27346  chebbnd1lem2  27403  chebbnd1lem3  27404  pntlemr  27535  ex-exp  30422  420gcd8e4  42039  420lcm8e840  42044  lcmineqlem23  42084  3lexlogpow2ineq2  42092  sum9cubes  42705  fmtno4prmfac  47603  139prmALT  47627  mod42tp1mod8  47633  3exp4mod41  47647  41prothprm  47650  8even  47744  2exp340mod341  47764  8exp8mod9  47767  pgnbgreunbgrlem4  48150