Theorem 4t2e8 12433

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7413   + caddc 11127   · cmul 11129  2c2 12319  4c4 12321  8c8 12325

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 2147  ax-9 2155  ax-ext 2732  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-mulcl 11186  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-1rid 11194  ax-cnre 11197

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 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333

This theorem is used by:  2t4e8  12434  8th4div3  12488  4t3e12  12839  cu2  14264  sqoddm1div8  14307  2exp7  17179  8nprm  17203  19prm  17210  139prm  17216  1259lem2  17224  1259lem3  17225  1259lem4  17226  2503lem1  17229  2503lem2  17230  4001lem1  17233  4001lem2  17234  log2tlbnd  27182  log2ub  27186  bpos1  27519  bposlem8  27527  lgsdir2lem2  27562  2lgslem3a  27632  2lgslem3b  27633  2lgslem3c  27634  2lgslem3d  27635  2lgsoddprmlem2  27645  2lgsoddprmlem3c  27648  chebbnd1lem2  27706  chebbnd1lem3  27707  pntlemr  27838  420gcd8e4  42872  420lcm8e840  42877  sum9cubes  43518  sin5tlem4  47740  goldratmolem2  47751  139prmALT  48499  41prothprm  48522  8even  48629  pgnbgreunbgrlem4  49035