Theorem 2t1e2 12301

Description: 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
2t1e2	⊢ (2 · 1) = 2

Proof of Theorem 2t1e2

Step	Hyp	Ref	Expression
1		2cn 12218	. 2 ⊢ 2 ∈ ℂ
2	1	mulridi 11134	1 ⊢ (2 · 1) = 2

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   · cmul 11029  2c2 12198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-mulcom 11088  ax-mulass 11090  ax-distr 11091  ax-1rid 11094  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-2 12206

This theorem is referenced by:  decbin2  12746  expubnd  14099  01sqrexlem7  15169  trirecip  15784  bpoly3  15979  fsumcube  15981  ege2le3  16011  cos2tsin  16102  cos2bnd  16111  odd2np1  16266  opoe  16288  flodddiv4  16340  2mulprm  16618  pythagtriplem4  16745  2503lem2  17063  2503lem3  17064  4001lem4  17069  4001prm  17070  htpycc  24933  pco1  24969  pcohtpylem  24973  pcopt  24976  pcorevlem  24980  ovolunlem1a  25451  cos2pi  26439  coskpi  26486  dcubic2  26808  dcubic  26810  basellem3  27047  chtublem  27176  bcp1ctr  27244  bclbnd  27245  bposlem1  27249  bposlem2  27250  bposlem5  27253  2lgslem3d1  27368  2sqreultlem  27412  2sqreunnltlem  27415  chebbnd1lem1  27434  chebbnd1lem3  27436  chebbnd1  27437  frgrregord013  30419  ex-ind-dvds  30485  wrdt2ind  32984  knoppndvlem12  36666  heiborlem6  37956  3lexlogpow5ineq1  42247  aks4d1p1  42269  2np3bcnp1  42337  2ap1caineq  42338  flt4lem7  42844  jm2.23  43180  sumnnodd  45818  wallispilem4  46254  wallispi2lem1  46257  wallispi2lem2  46258  wallispi2  46259  stirlinglem11  46270  dirkertrigeqlem1  46284  fouriersw  46417  fmtnorec4  47737  lighneallem2  47794  lighneallem3  47795  3exp4mod41  47804  opoeALTV  47871  fppr2odd  47919  8exp8mod9  47924  ackval2  48870  ackval2012  48879