Theorem 4t2e8 12432

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 12349	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12403	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12419	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2763	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1537  (class class class)co 7431   + caddc 11156   · cmul 11158  2c2 12319  4c4 12321  8c8 12325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-mulcl 11215  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-1rid 11223  ax-cnre 11226

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333

This theorem is referenced by:  8th4div3  12484  4t3e12  12829  sq4e2t8  14235  cu2  14236  sqoddm1div8  14279  cos2bnd  16221  2exp7  17122  2exp8  17123  8nprm  17146  19prm  17152  139prm  17158  1259lem2  17166  1259lem3  17167  1259lem4  17168  1259lem5  17169  2503lem1  17171  2503lem2  17172  4001lem1  17175  4001lem2  17176  4001lem3  17177  4001lem4  17178  quart1lem  26913  quart1  26914  quartlem1  26915  log2tlbnd  27003  log2ub  27007  bpos1  27342  bposlem8  27350  lgsdir2lem2  27385  2lgslem3a  27455  2lgslem3b  27456  2lgslem3c  27457  2lgslem3d  27458  2lgsoddprmlem2  27468  2lgsoddprmlem3c  27471  2lgsoddprmlem3d  27472  chebbnd1lem2  27529  chebbnd1lem3  27530  pntlemr  27661  ex-exp  30479  420gcd8e4  41988  420lcm8e840  41993  lcmineqlem23  42033  3lexlogpow2ineq2  42041  sum9cubes  42659  fmtno4prmfac  47497  139prmALT  47521  mod42tp1mod8  47527  3exp4mod41  47541  41prothprm  47544  8even  47638  2exp340mod341  47658  8exp8mod9  47661