Theorem 2t1e2 12429

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

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   · cmul 11160  2c2 12321

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329

This theorem is referenced by:  decbin2  12874  expubnd  14217  01sqrexlem7  15287  trirecip  15899  bpoly3  16094  fsumcube  16096  ege2le3  16126  cos2tsin  16215  cos2bnd  16224  odd2np1  16378  opoe  16400  flodddiv4  16452  2mulprm  16730  pythagtriplem4  16857  2503lem2  17175  2503lem3  17176  4001lem4  17181  4001prm  17182  htpycc  25012  pco1  25048  pcohtpylem  25052  pcopt  25055  pcorevlem  25059  ovolunlem1a  25531  cos2pi  26518  coskpi  26565  dcubic2  26887  dcubic  26889  basellem3  27126  chtublem  27255  bcp1ctr  27323  bclbnd  27324  bposlem1  27328  bposlem2  27329  bposlem5  27332  2lgslem3d1  27447  2sqreultlem  27491  2sqreunnltlem  27494  chebbnd1lem1  27513  chebbnd1lem3  27515  chebbnd1  27516  frgrregord013  30414  ex-ind-dvds  30480  wrdt2ind  32938  knoppndvlem12  36524  heiborlem6  37823  3lexlogpow5ineq1  42055  aks4d1p1  42077  2np3bcnp1  42145  2ap1caineq  42146  flt4lem7  42669  jm2.23  43008  sumnnodd  45645  wallispilem4  46083  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem11  46099  dirkertrigeqlem1  46113  fouriersw  46246  fmtnorec4  47536  lighneallem2  47593  lighneallem3  47594  3exp4mod41  47603  opoeALTV  47670  fppr2odd  47718  8exp8mod9  47723  ackval2  48603  ackval2012  48612