Theorem 4t2e8 12409

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 12326	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12379	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12395	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2792	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1567  (class class class)co 7411   + caddc 11103   · cmul 11105  2c2 12295  4c4 12297  8c8 12301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-mulcl 11162  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-1rid 11170  ax-cnre 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309

This theorem is referenced by:  2t4e8  12410  8th4div3  12464  4t3e12  12814  sq4e2t8  14235  cu2  14236  sqoddm1div8  14279  cos2bnd  16244  2exp7  17147  2exp8  17148  8nprm  17171  19prm  17178  139prm  17184  1259lem2  17192  1259lem3  17193  1259lem4  17194  1259lem5  17195  2503lem1  17197  2503lem2  17198  4001lem1  17201  4001lem2  17202  4001lem3  17203  4001lem4  17204  quart1lem  26986  quart1  26987  quartlem1  26988  log2tlbnd  27076  log2ub  27080  bpos1  27413  bposlem8  27421  lgsdir2lem2  27456  2lgslem3a  27526  2lgslem3b  27527  2lgslem3c  27528  2lgslem3d  27529  2lgsoddprmlem2  27539  2lgsoddprmlem3c  27542  2lgsoddprmlem3d  27543  chebbnd1lem2  27600  chebbnd1lem3  27601  pntlemr  27732  ex-exp  30742  420gcd8e4  42697  420lcm8e840  42702  lcmineqlem23  42742  3lexlogpow2ineq2  42750  sum9cubes  43330  sin5tlem4  47536  goldratmolem2  47546  fmtno4prmfac  48247  139prmALT  48271  3exp4mod41  48291  41prothprm  48294  8even  48401  2exp340mod341  48421  8exp8mod9  48424  pgnbgreunbgrlem4  48807