Theorem 4t2e8 12291

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

Syntax hints:   = wceq 1540  (class class class)co 7349   + caddc 11012   · cmul 11014  2c2 12183  4c4 12185  8c8 12189

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 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-1rid 11079  ax-cnre 11082

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196  df-8 12197

This theorem is referenced by:  8th4div3  12344  4t3e12  12689  sq4e2t8  14106  cu2  14107  sqoddm1div8  14150  cos2bnd  16097  2exp7  16999  2exp8  17000  8nprm  17023  19prm  17029  139prm  17035  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  quart1lem  26763  quart1  26764  quartlem1  26765  log2tlbnd  26853  log2ub  26857  bpos1  27192  bposlem8  27200  lgsdir2lem2  27235  2lgslem3a  27305  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  2lgsoddprmlem2  27318  2lgsoddprmlem3c  27321  2lgsoddprmlem3d  27322  chebbnd1lem2  27379  chebbnd1lem3  27380  pntlemr  27511  ex-exp  30398  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