Theorem 4t2e8 11808

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 11725	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 11779	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 11795	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2846	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1537  (class class class)co 7158   + caddc 10542   · cmul 10544  2c2 11695  4c4 11697  8c8 11701

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-1rid 10609  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709

This theorem is referenced by:  8th4div3  11860  4t3e12  12199  sq4e2t8  13565  cu2  13566  sqoddm1div8  13607  cos2bnd  15543  2exp8  16425  8nprm  16447  19prm  16453  139prm  16459  1259lem2  16467  1259lem3  16468  1259lem4  16469  1259lem5  16470  2503lem1  16472  2503lem2  16473  4001lem1  16476  4001lem2  16477  4001lem3  16478  4001lem4  16479  quart1lem  25435  quart1  25436  quartlem1  25437  log2tlbnd  25525  log2ub  25529  bpos1  25861  bposlem8  25869  lgsdir2lem2  25904  2lgslem3a  25974  2lgslem3b  25975  2lgslem3c  25976  2lgslem3d  25977  2lgsoddprmlem2  25987  2lgsoddprmlem3c  25990  2lgsoddprmlem3d  25991  chebbnd1lem2  26048  chebbnd1lem3  26049  pntlemr  26180  ex-exp  28231  fmtno4prmfac  43741  139prmALT  43766  2exp7  43769  mod42tp1mod8  43774  3exp4mod41  43788  41prothprm  43791  8even  43885  2exp340mod341  43905  8exp8mod9  43908