Theorem 4t2e8 11793

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 11710	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 11764	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 11780	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2821	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1538  (class class class)co 7135   + caddc 10529   · cmul 10531  2c2 11680  4c4 11682  8c8 11686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694

This theorem is referenced by:  8th4div3  11845  4t3e12  12184  sq4e2t8  13558  cu2  13559  sqoddm1div8  13600  cos2bnd  15533  2exp7  16414  2exp8  16415  8nprm  16437  19prm  16443  139prm  16449  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem1  16462  2503lem2  16463  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  quart1lem  25441  quart1  25442  quartlem1  25443  log2tlbnd  25531  log2ub  25535  bpos1  25867  bposlem8  25875  lgsdir2lem2  25910  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2lgsoddprmlem2  25993  2lgsoddprmlem3c  25996  2lgsoddprmlem3d  25997  chebbnd1lem2  26054  chebbnd1lem3  26055  pntlemr  26186  ex-exp  28235  420gcd8e4  39294  420lcm8e840  39299  lcmineqlem23  39339  fmtno4prmfac  44089  139prmALT  44113  mod42tp1mod8  44120  3exp4mod41  44134  41prothprm  44137  8even  44231  2exp340mod341  44251  8exp8mod9  44254