Theorem 4t2e8 12356

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 12278	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12327	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12343	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2753	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1540  (class class class)co 7390   + caddc 11078   · cmul 11080  2c2 12248  4c4 12250  8c8 12254

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 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262

This theorem is referenced by:  8th4div3  12409  4t3e12  12754  sq4e2t8  14171  cu2  14172  sqoddm1div8  14215  cos2bnd  16163  2exp7  17065  2exp8  17066  8nprm  17089  19prm  17095  139prm  17101  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  quart1lem  26772  quart1  26773  quartlem1  26774  log2tlbnd  26862  log2ub  26866  bpos1  27201  bposlem8  27209  lgsdir2lem2  27244  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgsoddprmlem2  27327  2lgsoddprmlem3c  27330  2lgsoddprmlem3d  27331  chebbnd1lem2  27388  chebbnd1lem3  27389  pntlemr  27520  ex-exp  30386  420gcd8e4  42001  420lcm8e840  42006  lcmineqlem23  42046  3lexlogpow2ineq2  42054  sum9cubes  42667  fmtno4prmfac  47577  139prmALT  47601  mod42tp1mod8  47607  3exp4mod41  47621  41prothprm  47624  8even  47718  2exp340mod341  47738  8exp8mod9  47741  pgnbgreunbgrlem4  48113