Theorem 4t2e8 12420

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 12337	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12390	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12406	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2788	1 ⊢ (4 · 2) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7416   + caddc 11114   · cmul 11116  2c2 12306  4c4 12308  8c8 12312

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-mulcl 11173  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-1rid 11181  ax-cnre 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419  df-2 12314  df-3 12315  df-4 12316  df-5 12317  df-6 12318  df-7 12319  df-8 12320

This theorem is used by:  2t4e8  12421  8th4div3  12475  4t3e12  12826  cu2  14250  sqoddm1div8  14293  2exp7  17165  8nprm  17189  19prm  17196  139prm  17202  1259lem2  17210  1259lem3  17211  1259lem4  17212  2503lem1  17215  2503lem2  17216  4001lem1  17219  4001lem2  17220  log2tlbnd  27141  log2ub  27145  bpos1  27478  bposlem8  27486  lgsdir2lem2  27521  2lgslem3a  27591  2lgslem3b  27592  2lgslem3c  27593  2lgslem3d  27594  2lgsoddprmlem2  27604  2lgsoddprmlem3c  27607  chebbnd1lem2  27665  chebbnd1lem3  27666  pntlemr  27797  420gcd8e4  42806  420lcm8e840  42811  sum9cubes  43437  sin5tlem4  47646  goldratmolem2  47656  139prmALT  48381  41prothprm  48404  8even  48511  pgnbgreunbgrlem4  48917