Theorem 4t2e8 12335

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 12257	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12306	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12322	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2760	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1542  (class class class)co 7360   + caddc 11032   · cmul 11034  2c2 12227  4c4 12229  8c8 12233

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 2709  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-1rid 11099  ax-cnre 11102

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 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241

This theorem is referenced by:  8th4div3  12388  4t3e12  12733  sq4e2t8  14152  cu2  14153  sqoddm1div8  14196  cos2bnd  16146  2exp7  17049  2exp8  17050  8nprm  17073  19prm  17079  139prm  17085  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  quart1lem  26832  quart1  26833  quartlem1  26834  log2tlbnd  26922  log2ub  26926  bpos1  27260  bposlem8  27268  lgsdir2lem2  27303  2lgslem3a  27373  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  2lgsoddprmlem2  27386  2lgsoddprmlem3c  27389  2lgsoddprmlem3d  27390  chebbnd1lem2  27447  chebbnd1lem3  27448  pntlemr  27579  ex-exp  30535  420gcd8e4  42459  420lcm8e840  42464  lcmineqlem23  42504  3lexlogpow2ineq2  42512  sum9cubes  43119  sin5tlem4  47340  fmtno4prmfac  48047  139prmALT  48071  mod42tp1mod8  48077  3exp4mod41  48091  41prothprm  48094  8even  48201  2exp340mod341  48221  8exp8mod9  48224  pgnbgreunbgrlem4  48607