Theorem 2t4e8 12437

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 12353	. 2 ⊢ 4 ∈ ℂ
2		2cn 12343	. 2 ⊢ 2 ∈ ℂ
3		4t2e8 12436	. 2 ⊢ (4 · 2) = 8
4	1, 2, 3	mulcomli 11245	1 ⊢ (2 · 4) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7416   · cmul 11132  2c2 12322  4c4 12324  8c8 12328

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 2734  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

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 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336

This theorem is used by:  sq4e2t8  14265  cos2bnd  16280  2exp8  17184  1259lem5  17231  2503lem2  17234  4001lem1  17237  4001lem3  17239  4001lem4  17240  quart1lem  27093  quart1  27094  quartlem1  27095  log2ub  27187  bposlem8  27528  2lgslem3a  27633  2lgsoddprmlem3d  27650  ex-exp  30931  420lcm8e840  42879  lcmineqlem23  42919  3lexlogpow2ineq2  42927  sin5tlem1  47739  fmtno4prmfac  48477  mod42tp1mod8  48507  3exp4mod41  48521  2exp340mod341  48651  8exp8mod9  48654