Theorem 4t2e8 12344

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 12266	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12315	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12331	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2759	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1542  (class class class)co 7367   + caddc 11041   · cmul 11043  2c2 12236  4c4 12238  8c8 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250

This theorem is referenced by:  8th4div3  12397  4t3e12  12742  sq4e2t8  14161  cu2  14162  sqoddm1div8  14205  cos2bnd  16155  2exp7  17058  2exp8  17059  8nprm  17082  19prm  17088  139prm  17094  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  quart1lem  26819  quart1  26820  quartlem1  26821  log2tlbnd  26909  log2ub  26913  bpos1  27246  bposlem8  27254  lgsdir2lem2  27289  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgsoddprmlem2  27372  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  chebbnd1lem2  27433  chebbnd1lem3  27434  pntlemr  27565  ex-exp  30520  420gcd8e4  42445  420lcm8e840  42450  lcmineqlem23  42490  3lexlogpow2ineq2  42498  sum9cubes  43105  sin5tlem4  47324  goldratmolem2  47334  fmtno4prmfac  48035  139prmALT  48059  mod42tp1mod8  48065  3exp4mod41  48079  41prothprm  48082  8even  48189  2exp340mod341  48209  8exp8mod9  48212  pgnbgreunbgrlem4  48595