Theorem 4t2e8 12299

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 12221	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12270	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12286	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2756	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1541  (class class class)co 7355   + caddc 11020   · cmul 11022  2c2 12191  4c4 12193  8c8 12197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-mulcl 11079  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-1rid 11087  ax-cnre 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-2 12199  df-3 12200  df-4 12201  df-5 12202  df-6 12203  df-7 12204  df-8 12205

This theorem is referenced by:  8th4div3  12352  4t3e12  12696  sq4e2t8  14113  cu2  14114  sqoddm1div8  14157  cos2bnd  16104  2exp7  17006  2exp8  17007  8nprm  17030  19prm  17036  139prm  17042  1259lem2  17050  1259lem3  17051  1259lem4  17052  1259lem5  17053  2503lem1  17055  2503lem2  17056  4001lem1  17059  4001lem2  17060  4001lem3  17061  4001lem4  17062  quart1lem  26812  quart1  26813  quartlem1  26814  log2tlbnd  26902  log2ub  26906  bpos1  27241  bposlem8  27249  lgsdir2lem2  27284  2lgslem3a  27354  2lgslem3b  27355  2lgslem3c  27356  2lgslem3d  27357  2lgsoddprmlem2  27367  2lgsoddprmlem3c  27370  2lgsoddprmlem3d  27371  chebbnd1lem2  27428  chebbnd1lem3  27429  pntlemr  27560  ex-exp  30451  420gcd8e4  42172  420lcm8e840  42177  lcmineqlem23  42217  3lexlogpow2ineq2  42225  sum9cubes  42830  fmtno4prmfac  47734  139prmALT  47758  mod42tp1mod8  47764  3exp4mod41  47778  41prothprm  47781  8even  47875  2exp340mod341  47895  8exp8mod9  47898  pgnbgreunbgrlem4  48281