Theorem 2t4e8 12539

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 12455	. 2 ⊢ 4 ∈ ℂ
2		2cn 12445	. 2 ⊢ 2 ∈ ℂ
3		4t2e8 12538	. 2 ⊢ (4 · 2) = 8
4	1, 2, 3	mulcomli 11345	1 ⊢ (2 · 4) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7443   · cmul 11232  2c2 12424  4c4 12426  8c8 12430

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-mulcl 11289  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-1rid 11297  ax-cnre 11300

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-2 12432  df-3 12433  df-4 12434  df-5 12435  df-6 12436  df-7 12437  df-8 12438

This theorem is used by:  sq4e2t8  14369  cos2bnd  16385  2exp8  17295  1259lem5  17342  2503lem2  17345  4001lem1  17348  4001lem3  17350  4001lem4  17351  quart1lem  27213  quart1  27214  quartlem1  27215  log2ub  27307  bposlem8  27648  2lgslem3a  27753  2lgsoddprmlem3d  27770  ex-exp  31081  420lcm8e840  43253  lcmineqlem23  43293  3lexlogpow2ineq2  43301  sin5tlem1  48124  fmtno4prmfac  48862  mod42tp1mod8  48892  3exp4mod41  48906  2exp340mod341  49036  8exp8mod9  49039