Theorem 4t2e8 11806

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 11723	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 11777	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 11793	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2844	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1537  (class class class)co 7156   + caddc 10540   · cmul 10542  2c2 11693  4c4 11695  8c8 11699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-1rid 10607  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-2 11701  df-3 11702  df-4 11703  df-5 11704  df-6 11705  df-7 11706  df-8 11707

This theorem is referenced by:  8th4div3  11858  4t3e12  12197  sq4e2t8  13563  cu2  13564  sqoddm1div8  13605  cos2bnd  15541  2exp8  16423  8nprm  16445  19prm  16451  139prm  16457  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  2503lem1  16470  2503lem2  16471  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  quart1lem  25433  quart1  25434  quartlem1  25435  log2tlbnd  25523  log2ub  25527  bpos1  25859  bposlem8  25867  lgsdir2lem2  25902  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgsoddprmlem2  25985  2lgsoddprmlem3c  25988  2lgsoddprmlem3d  25989  chebbnd1lem2  26046  chebbnd1lem3  26047  pntlemr  26178  ex-exp  28229  fmtno4prmfac  43754  139prmALT  43779  2exp7  43782  mod42tp1mod8  43787  3exp4mod41  43801  41prothprm  43804  8even  43898  2exp340mod341  43918  8exp8mod9  43921