Theorem 2t1e2 12420

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11118   · cmul 11122  2c2 12312

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-mulcl 11179  ax-mulcom 11181  ax-mulass 11183  ax-distr 11184  ax-1rid 11187  ax-cnre 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320

This theorem is used by:  decbin2  12877  expubnd  14234  01sqrexlem7  15325  trirecip  15942  bpoly3  16136  fsumcube  16138  ege2le3  16168  cos2tsin  16259  cos2bnd  16268  odd2np1  16423  opoe  16445  flodddiv4  16497  2mulprm  16775  pythagtriplem4  16903  2503lem2  17222  2503lem3  17223  4001lem4  17228  4001prm  17229  htpycc  25192  pco1  25227  pcohtpylem  25231  pcopt  25234  pcorevlem  25238  ovolunlem1a  25708  cos2pi  26694  coskpi  26741  dcubic2  27062  dcubic  27064  basellem3  27300  chtublem  27428  bcp1ctr  27496  bclbnd  27497  bposlem1  27501  bposlem2  27502  bposlem5  27505  2lgslem3d1  27620  2sqreultlem  27664  2sqreunnltlem  27667  chebbnd1lem1  27686  chebbnd1lem3  27688  chebbnd1  27689  frgrregord013  30819  ex-ind-dvds  30885  wrdt2ind  33341  knoppndvlem12  37171  heiborlem6  38527  3lexlogpow5ineq1  42881  aks4d1p1  42903  2np3bcnp1  42971  2ap1caineq  42972  flt4lem7  43451  jm2.23  43783  sumnnodd  46406  wallispilem4  46842  wallispi2lem1  46845  wallispi2lem2  46846  wallispi2  46847  stirlinglem11  46858  dirkertrigeqlem1  46872  fouriersw  47005  fmtnorec4  48361  lighneallem2  48418  lighneallem3  48419  3exp4mod41  48428  opoeALTV  48508  fppr2odd  48556  8exp8mod9  48561  ackval2  49521  ackval2012  49530