Theorem 2t1e2 12456

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

Syntax hints:   = wceq 1537  (class class class)co 7448  1c1 11185   · cmul 11189  2c2 12348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-mulcom 11248  ax-mulass 11250  ax-distr 11251  ax-1rid 11254  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-2 12356

This theorem is referenced by:  decbin2  12899  expubnd  14227  01sqrexlem7  15297  trirecip  15911  bpoly3  16106  fsumcube  16108  ege2le3  16138  cos2tsin  16227  cos2bnd  16236  odd2np1  16389  opoe  16411  flodddiv4  16461  2mulprm  16740  pythagtriplem4  16866  2503lem2  17185  2503lem3  17186  4001lem4  17191  4001prm  17192  htpycc  25031  pco1  25067  pcohtpylem  25071  pcopt  25074  pcorevlem  25078  ovolunlem1a  25550  cos2pi  26536  coskpi  26583  dcubic2  26905  dcubic  26907  basellem3  27144  chtublem  27273  bcp1ctr  27341  bclbnd  27342  bposlem1  27346  bposlem2  27347  bposlem5  27350  2lgslem3d1  27465  2sqreultlem  27509  2sqreunnltlem  27512  chebbnd1lem1  27531  chebbnd1lem3  27533  chebbnd1  27534  frgrregord013  30427  ex-ind-dvds  30493  wrdt2ind  32920  knoppndvlem12  36489  heiborlem6  37776  3lexlogpow5ineq1  42011  aks4d1p1  42033  2np3bcnp1  42101  2ap1caineq  42102  flt4lem7  42614  jm2.23  42953  sumnnodd  45551  wallispilem4  45989  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem11  46005  dirkertrigeqlem1  46019  fouriersw  46152  fmtnorec4  47423  lighneallem2  47480  lighneallem3  47481  3exp4mod41  47490  opoeALTV  47557  fppr2odd  47605  8exp8mod9  47610  ackval2  48416  ackval2012  48425