Theorem 4t2e8 12504

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 12421	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12474	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12490	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2784	1 ⊢ (4 · 2) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7418   + caddc 11196   · cmul 11198  2c2 12390  4c4 12392  8c8 12396

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 2733  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-mulcl 11255  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-1rid 11263  ax-cnre 11266

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 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  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 6493  df-fv 6545  df-ov 7421  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403  df-8 12404

This theorem is used by:  2t4e8  12505  8th4div3  12559  4t3e12  12910  cu2  14336  sqoddm1div8  14380  2exp7  17258  8nprm  17282  19prm  17289  139prm  17295  1259lem2  17303  1259lem3  17304  1259lem4  17305  2503lem1  17308  2503lem2  17309  4001lem1  17312  4001lem2  17313  log2tlbnd  27266  log2ub  27270  bpos1  27603  bposlem8  27611  lgsdir2lem2  27646  2lgslem3a  27716  2lgslem3b  27717  2lgslem3c  27718  2lgslem3d  27719  2lgsoddprmlem2  27729  2lgsoddprmlem3c  27732  chebbnd1lem2  27790  chebbnd1lem3  27791  pntlemr  27922  420gcd8e4  43036  420lcm8e840  43041  sum9cubes  43663  sin5tlem4  47891  goldratmolem2  47902  139prmALT  48650  41prothprm  48673  8even  48780  pgnbgreunbgrlem4  49186