Theorem 4t2e8 12551

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 12468	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12521	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12537	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2786	1 ⊢ (4 · 2) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451   + caddc 11242   · cmul 11244  2c2 12437  4c4 12439  8c8 12443

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-1rid 11309  ax-cnre 11312

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450  df-8 12451

This theorem is used by:  2t4e8  12552  8th4div3  12606  4t3e12  12957  cu2  14383  sqoddm1div8  14428  2exp7  17309  8nprm  17333  19prm  17340  139prm  17346  1259lem2  17354  1259lem3  17355  1259lem4  17356  2503lem1  17359  2503lem2  17360  4001lem1  17363  4001lem2  17364  log2tlbnd  27330  log2ub  27334  bpos1  27667  bposlem8  27675  lgsdir2lem2  27710  2lgslem3a  27780  2lgslem3b  27781  2lgslem3c  27782  2lgslem3d  27783  2lgsoddprmlem2  27793  2lgsoddprmlem3c  27796  chebbnd1lem2  27854  chebbnd1lem3  27855  pntlemr  27986  420gcd8e4  43322  420lcm8e840  43327  sum9cubes  43949  sin5tlem4  48195  goldratmolem2  48206  139prmALT  48954  41prothprm  48977  8even  49084  pgnbgreunbgrlem4  49490