Theorem 2t1e2 12426

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

Syntax hints:   = wceq 1536  (class class class)co 7430  1c1 11153   · cmul 11157  2c2 12318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulcom 11216  ax-mulass 11218  ax-distr 11219  ax-1rid 11222  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-2 12326

This theorem is referenced by:  decbin2  12871  expubnd  14213  01sqrexlem7  15283  trirecip  15895  bpoly3  16090  fsumcube  16092  ege2le3  16122  cos2tsin  16211  cos2bnd  16220  odd2np1  16374  opoe  16396  flodddiv4  16448  2mulprm  16726  pythagtriplem4  16852  2503lem2  17171  2503lem3  17172  4001lem4  17177  4001prm  17178  htpycc  25025  pco1  25061  pcohtpylem  25065  pcopt  25068  pcorevlem  25072  ovolunlem1a  25544  cos2pi  26532  coskpi  26579  dcubic2  26901  dcubic  26903  basellem3  27140  chtublem  27269  bcp1ctr  27337  bclbnd  27338  bposlem1  27342  bposlem2  27343  bposlem5  27346  2lgslem3d1  27461  2sqreultlem  27505  2sqreunnltlem  27508  chebbnd1lem1  27527  chebbnd1lem3  27529  chebbnd1  27530  frgrregord013  30423  ex-ind-dvds  30489  wrdt2ind  32922  knoppndvlem12  36505  heiborlem6  37802  3lexlogpow5ineq1  42035  aks4d1p1  42057  2np3bcnp1  42125  2ap1caineq  42126  flt4lem7  42645  jm2.23  42984  sumnnodd  45585  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem11  46039  dirkertrigeqlem1  46053  fouriersw  46186  fmtnorec4  47473  lighneallem2  47530  lighneallem3  47531  3exp4mod41  47540  opoeALTV  47607  fppr2odd  47655  8exp8mod9  47660  ackval2  48531  ackval2012  48540