Theorem 4t2e8 12384

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 12301	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12355	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12371	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2760	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1541  (class class class)co 7411   + caddc 11115   · cmul 11117  2c2 12271  4c4 12273  8c8 12277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-mulcl 11174  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-1rid 11182  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285

This theorem is referenced by:  8th4div3  12436  4t3e12  12779  sq4e2t8  14167  cu2  14168  sqoddm1div8  14210  cos2bnd  16135  2exp7  17025  2exp8  17026  8nprm  17049  19prm  17055  139prm  17061  1259lem2  17069  1259lem3  17070  1259lem4  17071  1259lem5  17072  2503lem1  17074  2503lem2  17075  4001lem1  17078  4001lem2  17079  4001lem3  17080  4001lem4  17081  quart1lem  26584  quart1  26585  quartlem1  26586  log2tlbnd  26674  log2ub  26678  bpos1  27010  bposlem8  27018  lgsdir2lem2  27053  2lgslem3a  27123  2lgslem3b  27124  2lgslem3c  27125  2lgslem3d  27126  2lgsoddprmlem2  27136  2lgsoddprmlem3c  27139  2lgsoddprmlem3d  27140  chebbnd1lem2  27197  chebbnd1lem3  27198  pntlemr  27329  ex-exp  29958  420gcd8e4  41177  420lcm8e840  41182  lcmineqlem23  41222  3lexlogpow2ineq2  41230  sum9cubes  41716  fmtno4prmfac  46539  139prmALT  46563  mod42tp1mod8  46569  3exp4mod41  46583  41prothprm  46586  8even  46680  2exp340mod341  46700  8exp8mod9  46703