Theorem 2t3e6 12536

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

Assertion

Ref	Expression
2t3e6	⊢ (2 · 3) = 6

Proof of Theorem 2t3e6

Step	Hyp	Ref	Expression
1		3cn 12451	. 2 ⊢ 3 ∈ ℂ
2		2cn 12445	. 2 ⊢ 2 ∈ ℂ
3		3t2e6 12535	. 2 ⊢ (3 · 2) = 6
4	1, 2, 3	mulcomli 11345	1 ⊢ (2 · 3) = 6

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7443   · cmul 11232  2c2 12424  3c3 12425  6c6 12428

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

This theorem is used by:  8th4div3  12593  halfthird  12594  fac3  14451  prmo3  17248  2exp6  17293  7prm  17317  83prm  17330  1259lem3  17340  1259lem4  17341  1259lem5  17342  2503lem2  17345  quart1  27214  log2ublem2  27305  log2ublem3  27306  log2ub  27307  basellem8  27445  cht3  27530  ppiub  27561  bclbnd  27637  bposlem8  27648  2lgsoddprmlem3d  27770  hgt750lem2  35351  3exp7  43295  25or6to4  43448  3cubeslem3l  43889  mod42tp1mod8  48892  2exp340mod341  49036