Theorem 2t1e2 12408

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 12320	. 2 ⊢ 2 ∈ ℂ
2	1	mulridi 11244	1 ⊢ (2 · 1) = 2

Syntax hints:   = wceq 1540  (class class class)co 7410  1c1 11135   · cmul 11139  2c2 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-mulcl 11196  ax-mulcom 11198  ax-mulass 11200  ax-distr 11201  ax-1rid 11204  ax-cnre 11207

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-2 12308

This theorem is referenced by:  decbin2  12854  expubnd  14201  01sqrexlem7  15272  trirecip  15884  bpoly3  16079  fsumcube  16081  ege2le3  16111  cos2tsin  16202  cos2bnd  16211  odd2np1  16365  opoe  16387  flodddiv4  16439  2mulprm  16717  pythagtriplem4  16844  2503lem2  17162  2503lem3  17163  4001lem4  17168  4001prm  17169  htpycc  24935  pco1  24971  pcohtpylem  24975  pcopt  24978  pcorevlem  24982  ovolunlem1a  25454  cos2pi  26442  coskpi  26489  dcubic2  26811  dcubic  26813  basellem3  27050  chtublem  27179  bcp1ctr  27247  bclbnd  27248  bposlem1  27252  bposlem2  27253  bposlem5  27256  2lgslem3d1  27371  2sqreultlem  27415  2sqreunnltlem  27418  chebbnd1lem1  27437  chebbnd1lem3  27439  chebbnd1  27440  frgrregord013  30381  ex-ind-dvds  30447  wrdt2ind  32934  knoppndvlem12  36546  heiborlem6  37845  3lexlogpow5ineq1  42072  aks4d1p1  42094  2np3bcnp1  42162  2ap1caineq  42163  flt4lem7  42649  jm2.23  42987  sumnnodd  45626  wallispilem4  46064  wallispi2lem1  46067  wallispi2lem2  46068  wallispi2  46069  stirlinglem11  46080  dirkertrigeqlem1  46094  fouriersw  46227  fmtnorec4  47530  lighneallem2  47587  lighneallem3  47588  3exp4mod41  47597  opoeALTV  47664  fppr2odd  47712  8exp8mod9  47717  ackval2  48629  ackval2012  48638