Theorem 2t3e6 12479

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 12394	. 2 ⊢ 3 ∈ ℂ
2		2cn 12388	. 2 ⊢ 2 ∈ ℂ
3		3t2e6 12478	. 2 ⊢ (3 · 2) = 6
4	1, 2, 3	mulcomli 11290	1 ⊢ (2 · 3) = 6

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7408   · cmul 11177  2c2 12367  3c3 12368  6c6 12371

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

This theorem is used by:  8th4div3  12536  halfthird  12537  fac3  14392  prmo3  17181  2exp6  17226  7prm  17250  83prm  17263  1259lem3  17273  1259lem4  17274  1259lem5  17275  2503lem2  17278  quart1  27148  log2ublem2  27239  log2ublem3  27240  log2ub  27241  basellem8  27379  cht3  27464  ppiub  27495  bclbnd  27571  bposlem8  27582  2lgsoddprmlem3d  27704  hgt750lem2  35216  3exp7  43023  25or6to4  43176  3cubeslem3l  43635  mod42tp1mod8  48609  2exp340mod341  48753