Theorem 2t1e2 12333

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

Syntax hints:   = wceq 1542  (class class class)co 7361  1c1 11033   · cmul 11037  2c2 12230

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 2709  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-mulcom 11096  ax-mulass 11098  ax-distr 11099  ax-1rid 11102  ax-cnre 11105

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 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238

This theorem is referenced by:  decbin2  12779  expubnd  14134  01sqrexlem7  15204  trirecip  15822  bpoly3  16017  fsumcube  16019  ege2le3  16049  cos2tsin  16140  cos2bnd  16149  odd2np1  16304  opoe  16326  flodddiv4  16378  2mulprm  16656  pythagtriplem4  16784  2503lem2  17102  2503lem3  17103  4001lem4  17108  4001prm  17109  htpycc  24960  pco1  24995  pcohtpylem  24999  pcopt  25002  pcorevlem  25006  ovolunlem1a  25476  cos2pi  26456  coskpi  26503  dcubic2  26824  dcubic  26826  basellem3  27063  chtublem  27191  bcp1ctr  27259  bclbnd  27260  bposlem1  27264  bposlem2  27265  bposlem5  27268  2lgslem3d1  27383  2sqreultlem  27427  2sqreunnltlem  27430  chebbnd1lem1  27449  chebbnd1lem3  27451  chebbnd1  27452  frgrregord013  30483  ex-ind-dvds  30549  wrdt2ind  33031  knoppndvlem12  36802  heiborlem6  38154  3lexlogpow5ineq1  42510  aks4d1p1  42532  2np3bcnp1  42600  2ap1caineq  42601  flt4lem7  43109  jm2.23  43445  sumnnodd  46081  wallispilem4  46517  wallispi2lem1  46520  wallispi2lem2  46521  wallispi2  46522  stirlinglem11  46533  dirkertrigeqlem1  46547  fouriersw  46680  fmtnorec4  48027  lighneallem2  48084  lighneallem3  48085  3exp4mod41  48094  opoeALTV  48174  fppr2odd  48222  8exp8mod9  48227  ackval2  49173  ackval2012  49182