Theorem 4t2e8 12380

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 12297	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12350	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12366	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2784	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1559  (class class class)co 7391   + caddc 11070   · cmul 11072  2c2 12266  4c4 12268  8c8 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-mulcl 11129  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-1rid 11137  ax-cnre 11140

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280

This theorem is referenced by:  2t4e8  12381  8th4div3  12435  4t3e12  12785  sq4e2t8  14206  cu2  14207  sqoddm1div8  14250  cos2bnd  16211  2exp7  17114  2exp8  17115  8nprm  17138  19prm  17145  139prm  17151  1259lem2  17159  1259lem3  17160  1259lem4  17161  1259lem5  17162  2503lem1  17164  2503lem2  17165  4001lem1  17168  4001lem2  17169  4001lem3  17170  4001lem4  17171  quart1lem  26908  quart1  26909  quartlem1  26910  log2tlbnd  26998  log2ub  27002  bpos1  27335  bposlem8  27343  lgsdir2lem2  27378  2lgslem3a  27448  2lgslem3b  27449  2lgslem3c  27450  2lgslem3d  27451  2lgsoddprmlem2  27461  2lgsoddprmlem3c  27464  2lgsoddprmlem3d  27465  chebbnd1lem2  27522  chebbnd1lem3  27523  pntlemr  27654  ex-exp  30609  420gcd8e4  42584  420lcm8e840  42589  lcmineqlem23  42629  3lexlogpow2ineq2  42637  sum9cubes  43215  sin5tlem4  47431  goldratmolem2  47441  fmtno4prmfac  48142  139prmALT  48166  3exp4mod41  48186  41prothprm  48189  8even  48296  2exp340mod341  48316  8exp8mod9  48319  pgnbgreunbgrlem4  48702