Theorem 2t1e2 11788

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

Syntax hints:   = wceq 1538  (class class class)co 7135  1c1 10527   · cmul 10531  2c2 11680

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688

This theorem is referenced by:  decbin2  12227  expubnd  13537  sqrlem7  14600  trirecip  15210  bpoly3  15404  fsumcube  15406  ege2le3  15435  cos2tsin  15524  cos2bnd  15533  odd2np1  15682  opoe  15704  flodddiv4  15754  2mulprm  16027  pythagtriplem4  16146  2503lem2  16463  2503lem3  16464  4001lem4  16469  4001prm  16470  htpycc  23585  pco1  23620  pcohtpylem  23624  pcopt  23627  pcorevlem  23631  ovolunlem1a  24100  cos2pi  25069  coskpi  25115  dcubic2  25430  dcubic  25432  basellem3  25668  chtublem  25795  bcp1ctr  25863  bclbnd  25864  bposlem1  25868  bposlem2  25869  bposlem5  25872  2lgslem3d1  25987  2sqreultlem  26031  2sqreunnltlem  26034  chebbnd1lem1  26053  chebbnd1lem3  26055  chebbnd1  26056  frgrregord013  28180  ex-ind-dvds  28246  wrdt2ind  30653  knoppndvlem12  33975  heiborlem6  35254  2np3bcnp1  39348  2ap1caineq  39349  jm2.23  39937  sumnnodd  42272  wallispilem4  42710  wallispi2lem1  42713  wallispi2lem2  42714  wallispi2  42715  stirlinglem11  42726  dirkertrigeqlem1  42740  fouriersw  42873  fmtnorec4  44066  lighneallem2  44124  lighneallem3  44125  3exp4mod41  44134  opoeALTV  44201  fppr2odd  44249  8exp8mod9  44254  ackval2  45096  ackval2012  45105