Theorem 2t1e2 12041

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 11953	. 2 ⊢ 2 ∈ ℂ
2	1	mulid1i 10885	1 ⊢ (2 · 1) = 2

Syntax hints:   = wceq 1543  (class class class)co 7252  1c1 10778   · cmul 10782  2c2 11933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-resscn 10834  ax-1cn 10835  ax-icn 10836  ax-addcl 10837  ax-mulcl 10839  ax-mulcom 10841  ax-mulass 10843  ax-distr 10844  ax-1rid 10847  ax-cnre 10850

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6373  df-fv 6423  df-ov 7255  df-2 11941

This theorem is referenced by:  decbin2  12482  expubnd  13798  sqrlem7  14863  trirecip  15478  bpoly3  15671  fsumcube  15673  ege2le3  15702  cos2tsin  15791  cos2bnd  15800  odd2np1  15953  opoe  15975  flodddiv4  16025  2mulprm  16301  pythagtriplem4  16423  2503lem2  16742  2503lem3  16743  4001lem4  16748  4001prm  16749  htpycc  24024  pco1  24059  pcohtpylem  24063  pcopt  24066  pcorevlem  24070  ovolunlem1a  24540  cos2pi  25513  coskpi  25559  dcubic2  25874  dcubic  25876  basellem3  26112  chtublem  26239  bcp1ctr  26307  bclbnd  26308  bposlem1  26312  bposlem2  26313  bposlem5  26316  2lgslem3d1  26431  2sqreultlem  26475  2sqreunnltlem  26478  chebbnd1lem1  26497  chebbnd1lem3  26499  chebbnd1  26500  frgrregord013  28635  ex-ind-dvds  28701  wrdt2ind  31102  knoppndvlem12  34605  heiborlem6  35880  3lexlogpow5ineq1  39969  aks4d1p1  39990  2np3bcnp1  40000  2ap1caineq  40001  flt4lem7  40384  jm2.23  40706  sumnnodd  43034  wallispilem4  43472  wallispi2lem1  43475  wallispi2lem2  43476  wallispi2  43477  stirlinglem11  43488  dirkertrigeqlem1  43502  fouriersw  43635  fmtnorec4  44862  lighneallem2  44919  lighneallem3  44920  3exp4mod41  44929  opoeALTV  44996  fppr2odd  45044  8exp8mod9  45049  ackval2  45889  ackval2012  45898