Theorem 4t2e8 12071

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 11988	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12042	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12058	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2766	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1539  (class class class)co 7255   + caddc 10805   · cmul 10807  2c2 11958  4c4 11960  8c8 11964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-1rid 10872  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970  df-7 11971  df-8 11972

This theorem is referenced by:  8th4div3  12123  4t3e12  12464  sq4e2t8  13844  cu2  13845  sqoddm1div8  13886  cos2bnd  15825  2exp7  16717  2exp8  16718  8nprm  16741  19prm  16747  139prm  16753  1259lem2  16761  1259lem3  16762  1259lem4  16763  1259lem5  16764  2503lem1  16766  2503lem2  16767  4001lem1  16770  4001lem2  16771  4001lem3  16772  4001lem4  16773  quart1lem  25910  quart1  25911  quartlem1  25912  log2tlbnd  26000  log2ub  26004  bpos1  26336  bposlem8  26344  lgsdir2lem2  26379  2lgslem3a  26449  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  2lgsoddprmlem2  26462  2lgsoddprmlem3c  26465  2lgsoddprmlem3d  26466  chebbnd1lem2  26523  chebbnd1lem3  26524  pntlemr  26655  ex-exp  28715  420gcd8e4  39942  420lcm8e840  39947  lcmineqlem23  39987  3lexlogpow2ineq2  39995  fmtno4prmfac  44912  139prmALT  44936  mod42tp1mod8  44942  3exp4mod41  44956  41prothprm  44959  8even  45053  2exp340mod341  45073  8exp8mod9  45076