Theorem 2t1e2 12293

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

Syntax hints:   = wceq 1541  (class class class)co 7355  1c1 11017   · cmul 11021  2c2 12190

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 2705  ax-resscn 11073  ax-1cn 11074  ax-icn 11075  ax-addcl 11076  ax-mulcl 11078  ax-mulcom 11080  ax-mulass 11082  ax-distr 11083  ax-1rid 11086  ax-cnre 11089

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 2712  df-cleq 2725  df-clel 2808  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-2 12198

This theorem is referenced by:  decbin2  12739  expubnd  14095  01sqrexlem7  15165  trirecip  15780  bpoly3  15975  fsumcube  15977  ege2le3  16007  cos2tsin  16098  cos2bnd  16107  odd2np1  16262  opoe  16284  flodddiv4  16336  2mulprm  16614  pythagtriplem4  16741  2503lem2  17059  2503lem3  17060  4001lem4  17065  4001prm  17066  htpycc  24916  pco1  24952  pcohtpylem  24956  pcopt  24959  pcorevlem  24963  ovolunlem1a  25434  cos2pi  26422  coskpi  26469  dcubic2  26791  dcubic  26793  basellem3  27030  chtublem  27159  bcp1ctr  27227  bclbnd  27228  bposlem1  27232  bposlem2  27233  bposlem5  27236  2lgslem3d1  27351  2sqreultlem  27395  2sqreunnltlem  27398  chebbnd1lem1  27417  chebbnd1lem3  27419  chebbnd1  27420  frgrregord013  30386  ex-ind-dvds  30452  wrdt2ind  32945  knoppndvlem12  36578  heiborlem6  37866  3lexlogpow5ineq1  42157  aks4d1p1  42179  2np3bcnp1  42247  2ap1caineq  42248  flt4lem7  42767  jm2.23  43103  sumnnodd  45744  wallispilem4  46180  wallispi2lem1  46183  wallispi2lem2  46184  wallispi2  46185  stirlinglem11  46196  dirkertrigeqlem1  46210  fouriersw  46343  fmtnorec4  47663  lighneallem2  47720  lighneallem3  47721  3exp4mod41  47730  opoeALTV  47797  fppr2odd  47845  8exp8mod9  47850  ackval2  48797  ackval2012  48806