Theorem 4t2e8 12405

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

Syntax hints:   = wceq 1567  (class class class)co 7408   + caddc 11099   · cmul 11101  2c2 12291  4c4 12293  8c8 12297

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 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-mulcl 11158  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-1rid 11166  ax-cnre 11169

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 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6490  df-fv 6542  df-ov 7411  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303  df-7 12304  df-8 12305

This theorem is referenced by:  2t4e8  12406  8th4div3  12460  4t3e12  12810  sq4e2t8  14231  cu2  14232  sqoddm1div8  14275  cos2bnd  16240  2exp7  17143  2exp8  17144  8nprm  17167  19prm  17174  139prm  17180  1259lem2  17188  1259lem3  17189  1259lem4  17190  1259lem5  17191  2503lem1  17193  2503lem2  17194  4001lem1  17197  4001lem2  17198  4001lem3  17199  4001lem4  17200  quart1lem  26982  quart1  26983  quartlem1  26984  log2tlbnd  27072  log2ub  27076  bpos1  27409  bposlem8  27417  lgsdir2lem2  27452  2lgslem3a  27522  2lgslem3b  27523  2lgslem3c  27524  2lgslem3d  27525  2lgsoddprmlem2  27535  2lgsoddprmlem3c  27538  2lgsoddprmlem3d  27539  chebbnd1lem2  27596  chebbnd1lem3  27597  pntlemr  27728  ex-exp  30738  420gcd8e4  42658  420lcm8e840  42663  lcmineqlem23  42703  3lexlogpow2ineq2  42711  sum9cubes  43291  sin5tlem4  47497  goldratmolem2  47507  fmtno4prmfac  48208  139prmALT  48232  3exp4mod41  48252  41prothprm  48255  8even  48362  2exp340mod341  48382  8exp8mod9  48385  pgnbgreunbgrlem4  48768