Theorem 4t2e8 12434

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 12351	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12405	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12421	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2765	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1540  (class class class)co 7431   + caddc 11158   · cmul 11160  2c2 12321  4c4 12323  8c8 12327

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335

This theorem is referenced by:  8th4div3  12486  4t3e12  12831  sq4e2t8  14238  cu2  14239  sqoddm1div8  14282  cos2bnd  16224  2exp7  17125  2exp8  17126  8nprm  17149  19prm  17155  139prm  17161  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  quart1lem  26898  quart1  26899  quartlem1  26900  log2tlbnd  26988  log2ub  26992  bpos1  27327  bposlem8  27335  lgsdir2lem2  27370  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2lgsoddprmlem2  27453  2lgsoddprmlem3c  27456  2lgsoddprmlem3d  27457  chebbnd1lem2  27514  chebbnd1lem3  27515  pntlemr  27646  ex-exp  30469  420gcd8e4  42007  420lcm8e840  42012  lcmineqlem23  42052  3lexlogpow2ineq2  42060  sum9cubes  42682  fmtno4prmfac  47559  139prmALT  47583  mod42tp1mod8  47589  3exp4mod41  47603  41prothprm  47606  8even  47700  2exp340mod341  47720  8exp8mod9  47723