Theorem 4t2e8 12320

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

Syntax hints:   = wceq 1542  (class class class)co 7368   + caddc 11041   · cmul 11043  2c2 12212  4c4 12214  8c8 12218

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 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 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226

This theorem is referenced by:  8th4div3  12373  4t3e12  12717  sq4e2t8  14134  cu2  14135  sqoddm1div8  14178  cos2bnd  16125  2exp7  17027  2exp8  17028  8nprm  17051  19prm  17057  139prm  17063  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  quart1lem  26833  quart1  26834  quartlem1  26835  log2tlbnd  26923  log2ub  26927  bpos1  27262  bposlem8  27270  lgsdir2lem2  27305  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2lgsoddprmlem2  27388  2lgsoddprmlem3c  27391  2lgsoddprmlem3d  27392  chebbnd1lem2  27449  chebbnd1lem3  27450  pntlemr  27581  ex-exp  30537  420gcd8e4  42376  420lcm8e840  42381  lcmineqlem23  42421  3lexlogpow2ineq2  42429  sum9cubes  43030  fmtno4prmfac  47932  139prmALT  47956  mod42tp1mod8  47962  3exp4mod41  47976  41prothprm  47979  8even  48073  2exp340mod341  48093  8exp8mod9  48096  pgnbgreunbgrlem4  48479