Theorem 2t4e8 12482

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 12398	. 2 ⊢ 4 ∈ ℂ
2		2cn 12388	. 2 ⊢ 2 ∈ ℂ
3		4t2e8 12481	. 2 ⊢ (4 · 2) = 8
4	1, 2, 3	mulcomli 11290	1 ⊢ (2 · 4) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7408   · cmul 11177  2c2 12367  4c4 12369  8c8 12373

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 11229  ax-1cn 11230  ax-icn 11231  ax-addcl 11232  ax-mulcl 11234  ax-mulcom 11236  ax-addass 11237  ax-mulass 11238  ax-distr 11239  ax-1rid 11242  ax-cnre 11245

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 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411  df-2 12375  df-3 12376  df-4 12377  df-5 12378  df-6 12379  df-7 12380  df-8 12381

This theorem is used by:  sq4e2t8  14311  cos2bnd  16324  2exp8  17228  1259lem5  17275  2503lem2  17278  4001lem1  17281  4001lem3  17283  4001lem4  17284  quart1lem  27147  quart1  27148  quartlem1  27149  log2ub  27241  bposlem8  27582  2lgslem3a  27687  2lgsoddprmlem3d  27704  ex-exp  30985  420lcm8e840  42981  lcmineqlem23  43021  3lexlogpow2ineq2  43029  sin5tlem1  47841  fmtno4prmfac  48579  mod42tp1mod8  48609  3exp4mod41  48623  2exp340mod341  48753  8exp8mod9  48756