Theorem 4t2e8 12416

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 12333	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12387	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12403	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2755	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1533  (class class class)co 7424   + caddc 11147   · cmul 11149  2c2 12303  4c4 12305  8c8 12309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-mulcl 11206  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-1rid 11214  ax-cnre 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rex 3067  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-iota 6503  df-fv 6559  df-ov 7427  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317

This theorem is referenced by:  8th4div3  12468  4t3e12  12811  sq4e2t8  14200  cu2  14201  sqoddm1div8  14243  cos2bnd  16170  2exp7  17062  2exp8  17063  8nprm  17086  19prm  17092  139prm  17098  1259lem2  17106  1259lem3  17107  1259lem4  17108  1259lem5  17109  2503lem1  17111  2503lem2  17112  4001lem1  17115  4001lem2  17116  4001lem3  17117  4001lem4  17118  quart1lem  26805  quart1  26806  quartlem1  26807  log2tlbnd  26895  log2ub  26899  bpos1  27234  bposlem8  27242  lgsdir2lem2  27277  2lgslem3a  27347  2lgslem3b  27348  2lgslem3c  27349  2lgslem3d  27350  2lgsoddprmlem2  27360  2lgsoddprmlem3c  27363  2lgsoddprmlem3d  27364  chebbnd1lem2  27421  chebbnd1lem3  27422  pntlemr  27553  ex-exp  30278  420gcd8e4  41481  420lcm8e840  41486  lcmineqlem23  41526  3lexlogpow2ineq2  41534  sum9cubes  42099  fmtno4prmfac  46914  139prmALT  46938  mod42tp1mod8  46944  3exp4mod41  46958  41prothprm  46961  8even  47055  2exp340mod341  47075  8exp8mod9  47078