Theorem 2t1e2 12305

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

Syntax hints:   = wceq 1541  (class class class)co 7358  1c1 11029   · cmul 11033  2c2 12202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulcom 11092  ax-mulass 11094  ax-distr 11095  ax-1rid 11098  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12210

This theorem is referenced by:  decbin2  12750  expubnd  14103  01sqrexlem7  15173  trirecip  15788  bpoly3  15983  fsumcube  15985  ege2le3  16015  cos2tsin  16106  cos2bnd  16115  odd2np1  16270  opoe  16292  flodddiv4  16344  2mulprm  16622  pythagtriplem4  16749  2503lem2  17067  2503lem3  17068  4001lem4  17073  4001prm  17074  htpycc  24937  pco1  24973  pcohtpylem  24977  pcopt  24980  pcorevlem  24984  ovolunlem1a  25455  cos2pi  26443  coskpi  26490  dcubic2  26812  dcubic  26814  basellem3  27051  chtublem  27180  bcp1ctr  27248  bclbnd  27249  bposlem1  27253  bposlem2  27254  bposlem5  27257  2lgslem3d1  27372  2sqreultlem  27416  2sqreunnltlem  27419  chebbnd1lem1  27438  chebbnd1lem3  27440  chebbnd1  27441  frgrregord013  30472  ex-ind-dvds  30538  wrdt2ind  33037  knoppndvlem12  36725  heiborlem6  38019  3lexlogpow5ineq1  42330  aks4d1p1  42352  2np3bcnp1  42420  2ap1caineq  42421  flt4lem7  42923  jm2.23  43259  sumnnodd  45897  wallispilem4  46333  wallispi2lem1  46336  wallispi2lem2  46337  wallispi2  46338  stirlinglem11  46349  dirkertrigeqlem1  46363  fouriersw  46496  fmtnorec4  47816  lighneallem2  47873  lighneallem3  47874  3exp4mod41  47883  opoeALTV  47950  fppr2odd  47998  8exp8mod9  48003  ackval2  48949  ackval2012  48958