Theorem 2t1e2 12331

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 12248	. 2 ⊢ 2 ∈ ℂ
2	1	mulridi 11141	1 ⊢ (2 · 1) = 2

Syntax hints:   = wceq 1547  (class class class)co 7357  1c1 11031   · cmul 11035  2c2 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-mulcl 11092  ax-mulcom 11094  ax-mulass 11096  ax-distr 11097  ax-1rid 11100  ax-cnre 11103

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-iota 6442  df-fv 6494  df-ov 7360  df-2 12236

This theorem is referenced by:  decbin2  12777  expubnd  14132  01sqrexlem7  15202  trirecip  15820  bpoly3  16015  fsumcube  16017  ege2le3  16047  cos2tsin  16138  cos2bnd  16147  odd2np1  16302  opoe  16324  flodddiv4  16376  2mulprm  16654  pythagtriplem4  16782  2503lem2  17100  2503lem3  17101  4001lem4  17106  4001prm  17107  htpycc  24966  pco1  25001  pcohtpylem  25005  pcopt  25008  pcorevlem  25012  ovolunlem1a  25482  cos2pi  26459  coskpi  26506  dcubic2  26827  dcubic  26829  basellem3  27065  chtublem  27193  bcp1ctr  27261  bclbnd  27262  bposlem1  27266  bposlem2  27267  bposlem5  27270  2lgslem3d1  27385  2sqreultlem  27429  2sqreunnltlem  27432  chebbnd1lem1  27451  chebbnd1lem3  27453  chebbnd1  27454  frgrregord013  30484  ex-ind-dvds  30550  wrdt2ind  33033  knoppndvlem12  36838  heiborlem6  38192  3lexlogpow5ineq1  42548  aks4d1p1  42570  2np3bcnp1  42638  2ap1caineq  42639  flt4lem7  43118  jm2.23  43450  sumnnodd  46083  wallispilem4  46519  wallispi2lem1  46522  wallispi2lem2  46523  wallispi2  46524  stirlinglem11  46535  dirkertrigeqlem1  46549  fouriersw  46682  fmtnorec4  48035  lighneallem2  48092  lighneallem3  48093  3exp4mod41  48102  opoeALTV  48182  fppr2odd  48230  8exp8mod9  48235  ackval2  49181  ackval2012  49190