Theorem 2t1e2 11850

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

Syntax hints:   = wceq 1538  (class class class)co 7156  1c1 10589   · cmul 10593  2c2 11742

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 2729  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-mulcl 10650  ax-mulcom 10652  ax-mulass 10654  ax-distr 10655  ax-1rid 10658  ax-cnre 10661

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-iota 6299  df-fv 6348  df-ov 7159  df-2 11750

This theorem is referenced by:  decbin2  12291  expubnd  13604  sqrlem7  14669  trirecip  15279  bpoly3  15473  fsumcube  15475  ege2le3  15504  cos2tsin  15593  cos2bnd  15602  odd2np1  15755  opoe  15777  flodddiv4  15827  2mulprm  16102  pythagtriplem4  16224  2503lem2  16542  2503lem3  16543  4001lem4  16548  4001prm  16549  htpycc  23694  pco1  23729  pcohtpylem  23733  pcopt  23736  pcorevlem  23740  ovolunlem1a  24209  cos2pi  25181  coskpi  25227  dcubic2  25542  dcubic  25544  basellem3  25780  chtublem  25907  bcp1ctr  25975  bclbnd  25976  bposlem1  25980  bposlem2  25981  bposlem5  25984  2lgslem3d1  26099  2sqreultlem  26143  2sqreunnltlem  26146  chebbnd1lem1  26165  chebbnd1lem3  26167  chebbnd1  26168  frgrregord013  28292  ex-ind-dvds  28358  wrdt2ind  30761  knoppndvlem12  34286  heiborlem6  35568  3lexlogpow5ineq1  39655  aks4d1p1  39676  2np3bcnp1  39679  2ap1caineq  39680  flt4lem7  40023  jm2.23  40345  sumnnodd  42673  wallispilem4  43111  wallispi2lem1  43114  wallispi2lem2  43115  wallispi2  43116  stirlinglem11  43127  dirkertrigeqlem1  43141  fouriersw  43274  fmtnorec4  44483  lighneallem2  44540  lighneallem3  44541  3exp4mod41  44550  opoeALTV  44617  fppr2odd  44665  8exp8mod9  44670  ackval2  45510  ackval2012  45519