Theorem 2t1e2 12339

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

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   · cmul 11043  2c2 12236

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244

This theorem is referenced by:  decbin2  12785  expubnd  14140  01sqrexlem7  15210  trirecip  15828  bpoly3  16023  fsumcube  16025  ege2le3  16055  cos2tsin  16146  cos2bnd  16155  odd2np1  16310  opoe  16332  flodddiv4  16384  2mulprm  16662  pythagtriplem4  16790  2503lem2  17108  2503lem3  17109  4001lem4  17114  4001prm  17115  htpycc  24947  pco1  24982  pcohtpylem  24986  pcopt  24989  pcorevlem  24993  ovolunlem1a  25463  cos2pi  26440  coskpi  26487  dcubic2  26808  dcubic  26810  basellem3  27046  chtublem  27174  bcp1ctr  27242  bclbnd  27243  bposlem1  27247  bposlem2  27248  bposlem5  27251  2lgslem3d1  27366  2sqreultlem  27410  2sqreunnltlem  27413  chebbnd1lem1  27432  chebbnd1lem3  27434  chebbnd1  27435  frgrregord013  30465  ex-ind-dvds  30531  wrdt2ind  33013  knoppndvlem12  36783  heiborlem6  38137  3lexlogpow5ineq1  42493  aks4d1p1  42515  2np3bcnp1  42583  2ap1caineq  42584  flt4lem7  43092  jm2.23  43424  sumnnodd  46060  wallispilem4  46496  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem11  46512  dirkertrigeqlem1  46526  fouriersw  46659  fmtnorec4  48012  lighneallem2  48069  lighneallem3  48070  3exp4mod41  48079  opoeALTV  48159  fppr2odd  48207  8exp8mod9  48212  ackval2  49158  ackval2012  49167