Theorem 4t2e8 12408

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

Syntax hints:   = wceq 1540  (class class class)co 7405   + caddc 11132   · cmul 11134  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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-mulcl 11191  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-1rid 11199  ax-cnre 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  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:  8th4div3  12461  4t3e12  12806  sq4e2t8  14217  cu2  14218  sqoddm1div8  14261  cos2bnd  16206  2exp7  17107  2exp8  17108  8nprm  17131  19prm  17137  139prm  17143  1259lem2  17151  1259lem3  17152  1259lem4  17153  1259lem5  17154  2503lem1  17156  2503lem2  17157  4001lem1  17160  4001lem2  17161  4001lem3  17162  4001lem4  17163  quart1lem  26817  quart1  26818  quartlem1  26819  log2tlbnd  26907  log2ub  26911  bpos1  27246  bposlem8  27254  lgsdir2lem2  27289  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgsoddprmlem2  27372  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  chebbnd1lem2  27433  chebbnd1lem3  27434  pntlemr  27565  ex-exp  30431  420gcd8e4  42019  420lcm8e840  42024  lcmineqlem23  42064  3lexlogpow2ineq2  42072  sum9cubes  42695  fmtno4prmfac  47586  139prmALT  47610  mod42tp1mod8  47616  3exp4mod41  47630  41prothprm  47633  8even  47727  2exp340mod341  47747  8exp8mod9  47750