Theorem 2t1e2 12379

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

Syntax hints:   = wceq 1541  (class class class)co 7411  1c1 11113   · cmul 11117  2c2 12271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-mulcl 11174  ax-mulcom 11176  ax-mulass 11178  ax-distr 11179  ax-1rid 11182  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-2 12279

This theorem is referenced by:  decbin2  12822  expubnd  14146  01sqrexlem7  15199  trirecip  15813  bpoly3  16006  fsumcube  16008  ege2le3  16037  cos2tsin  16126  cos2bnd  16135  odd2np1  16288  opoe  16310  flodddiv4  16360  2mulprm  16634  pythagtriplem4  16756  2503lem2  17075  2503lem3  17076  4001lem4  17081  4001prm  17082  htpycc  24720  pco1  24755  pcohtpylem  24759  pcopt  24762  pcorevlem  24766  ovolunlem1a  25237  cos2pi  26210  coskpi  26256  dcubic2  26573  dcubic  26575  basellem3  26811  chtublem  26938  bcp1ctr  27006  bclbnd  27007  bposlem1  27011  bposlem2  27012  bposlem5  27015  2lgslem3d1  27130  2sqreultlem  27174  2sqreunnltlem  27177  chebbnd1lem1  27196  chebbnd1lem3  27198  chebbnd1  27199  frgrregord013  29903  ex-ind-dvds  29969  wrdt2ind  32372  knoppndvlem12  35702  heiborlem6  36987  3lexlogpow5ineq1  41225  aks4d1p1  41247  2np3bcnp1  41266  2ap1caineq  41267  flt4lem7  41703  jm2.23  42037  sumnnodd  44645  wallispilem4  45083  wallispi2lem1  45086  wallispi2lem2  45087  wallispi2  45088  stirlinglem11  45099  dirkertrigeqlem1  45113  fouriersw  45246  fmtnorec4  46516  lighneallem2  46573  lighneallem3  46574  3exp4mod41  46583  opoeALTV  46650  fppr2odd  46698  8exp8mod9  46703  ackval2  47456  ackval2012  47465