Theorem 4t2e8 12349

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 12271	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12320	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12336	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2752	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1540  (class class class)co 7387   + caddc 11071   · cmul 11073  2c2 12241  4c4 12243  8c8 12247

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255

This theorem is referenced by:  8th4div3  12402  4t3e12  12747  sq4e2t8  14164  cu2  14165  sqoddm1div8  14208  cos2bnd  16156  2exp7  17058  2exp8  17059  8nprm  17082  19prm  17088  139prm  17094  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  quart1lem  26765  quart1  26766  quartlem1  26767  log2tlbnd  26855  log2ub  26859  bpos1  27194  bposlem8  27202  lgsdir2lem2  27237  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgsoddprmlem2  27320  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  chebbnd1lem2  27381  chebbnd1lem3  27382  pntlemr  27513  ex-exp  30379  420gcd8e4  41994  420lcm8e840  41999  lcmineqlem23  42039  3lexlogpow2ineq2  42047  sum9cubes  42660  fmtno4prmfac  47573  139prmALT  47597  mod42tp1mod8  47603  3exp4mod41  47617  41prothprm  47620  8even  47714  2exp340mod341  47734  8exp8mod9  47737  pgnbgreunbgrlem4  48109