Theorem 2t1e2 11025

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

Syntax hints:   = wceq 1474  (class class class)co 6526  1c1 9793   · cmul 9797  2c2 10919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rrecex 9864  ax-cnre 9865

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5753  df-fv 5797  df-ov 6529  df-2 10928

This theorem is referenced by:  decbin2  11517  expubnd  12740  sqrlem7  13785  trirecip  14382  bpoly3  14576  fsumcube  14578  ege2le3  14607  cos2tsin  14696  cos2bnd  14705  odd2np1  14851  opoe  14873  flodddiv4  14923  pythagtriplem4  15310  2503lem2  15631  2503lem3  15632  4001lem4  15637  4001prm  15638  htpycc  22534  pco1  22570  pcohtpylem  22574  pcopt  22577  pcorevlem  22581  ovolunlem1a  23015  cos2pi  23976  coskpi  24020  dcubic1lem  24314  dcubic2  24315  dcubic  24317  mcubic  24318  basellem3  24553  chtublem  24680  bcp1ctr  24748  bclbnd  24749  bposlem1  24753  bposlem2  24754  bposlem5  24757  2lgslem3d1  24872  chebbnd1lem1  24902  chebbnd1lem3  24904  chebbnd1  24905  frgraregord013  26438  ex-ind-dvds  26503  knoppndvlem12  31477  heiborlem6  32568  jm2.23  36364  sumnnodd  38480  wallispilem4  38744  wallispi2lem1  38747  wallispi2lem2  38748  wallispi2  38749  stirlinglem11  38760  dirkertrigeqlem1  38774  fouriersw  38907  fmtnorec4  39783  lighneallem2  39845  lighneallem3  39846  3exp4mod41  39855  opoeALTV  39916  av-frgraregord013  41530