Theorem 2t4e8 12513

Description: 2 times 4 equals 8. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
2t4e8	⊢ (2 · 4) = 8

Proof of Theorem 2t4e8

Step	Hyp	Ref	Expression
1		4cn 12429	. 2 ⊢ 4 ∈ ℂ
2		2cn 12419	. 2 ⊢ 2 ∈ ℂ
3		4t2e8 12512	. 2 ⊢ (4 · 2) = 8
4	1, 2, 3	mulcomli 11319	1 ⊢ (2 · 4) = 8

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7420   · cmul 11206  2c2 12398  4c4 12400  8c8 12404

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-mulcl 11263  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-1rid 11271  ax-cnre 11274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12406  df-3 12407  df-4 12408  df-5 12409  df-6 12410  df-7 12411  df-8 12412

This theorem is used by:  sq4e2t8  14343  cos2bnd  16357  2exp8  17267  1259lem5  17314  2503lem2  17317  4001lem1  17320  4001lem3  17322  4001lem4  17323  quart1lem  27184  quart1  27185  quartlem1  27186  log2ub  27278  bposlem8  27619  2lgslem3a  27724  2lgsoddprmlem3d  27741  ex-exp  31052  420lcm8e840  43137  lcmineqlem23  43177  3lexlogpow2ineq2  43185  sin5tlem1  47995  fmtno4prmfac  48733  mod42tp1mod8  48763  3exp4mod41  48777  2exp340mod341  48907  8exp8mod9  48910