Theorem 2t1e2 11801

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

Syntax hints:   = wceq 1537  (class class class)co 7156  1c1 10538   · cmul 10542  2c2 11693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-mulcom 10601  ax-mulass 10603  ax-distr 10604  ax-1rid 10607  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-2 11701

This theorem is referenced by:  decbin2  12240  expubnd  13542  sqrlem7  14608  trirecip  15218  bpoly3  15412  fsumcube  15414  ege2le3  15443  cos2tsin  15532  cos2bnd  15541  odd2np1  15690  opoe  15712  flodddiv4  15764  2mulprm  16037  pythagtriplem4  16156  2503lem2  16471  2503lem3  16472  4001lem4  16477  4001prm  16478  htpycc  23584  pco1  23619  pcohtpylem  23623  pcopt  23626  pcorevlem  23630  ovolunlem1a  24097  cos2pi  25062  coskpi  25108  dcubic2  25422  dcubic  25424  basellem3  25660  chtublem  25787  bcp1ctr  25855  bclbnd  25856  bposlem1  25860  bposlem2  25861  bposlem5  25864  2lgslem3d1  25979  2sqreultlem  26023  2sqreunnltlem  26026  chebbnd1lem1  26045  chebbnd1lem3  26047  chebbnd1  26048  frgrregord013  28174  ex-ind-dvds  28240  wrdt2ind  30627  knoppndvlem12  33862  heiborlem6  35109  jm2.23  39613  sumnnodd  41931  wallispilem4  42373  wallispi2lem1  42376  wallispi2lem2  42377  wallispi2  42378  stirlinglem11  42389  dirkertrigeqlem1  42403  fouriersw  42536  fmtnorec4  43731  lighneallem2  43791  lighneallem3  43792  3exp4mod41  43801  opoeALTV  43868  fppr2odd  43916  8exp8mod9  43921