Theorem 2t1e2 12344

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   · cmul 11073  2c2 12241

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249

This theorem is referenced by:  decbin2  12790  expubnd  14143  01sqrexlem7  15214  trirecip  15829  bpoly3  16024  fsumcube  16026  ege2le3  16056  cos2tsin  16147  cos2bnd  16156  odd2np1  16311  opoe  16333  flodddiv4  16385  2mulprm  16663  pythagtriplem4  16790  2503lem2  17108  2503lem3  17109  4001lem4  17114  4001prm  17115  htpycc  24879  pco1  24915  pcohtpylem  24919  pcopt  24922  pcorevlem  24926  ovolunlem1a  25397  cos2pi  26385  coskpi  26432  dcubic2  26754  dcubic  26756  basellem3  26993  chtublem  27122  bcp1ctr  27190  bclbnd  27191  bposlem1  27195  bposlem2  27196  bposlem5  27199  2lgslem3d1  27314  2sqreultlem  27358  2sqreunnltlem  27361  chebbnd1lem1  27380  chebbnd1lem3  27382  chebbnd1  27383  frgrregord013  30324  ex-ind-dvds  30390  wrdt2ind  32875  knoppndvlem12  36511  heiborlem6  37810  3lexlogpow5ineq1  42042  aks4d1p1  42064  2np3bcnp1  42132  2ap1caineq  42133  flt4lem7  42647  jm2.23  42985  sumnnodd  45628  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem11  46082  dirkertrigeqlem1  46096  fouriersw  46229  fmtnorec4  47550  lighneallem2  47607  lighneallem3  47608  3exp4mod41  47617  opoeALTV  47684  fppr2odd  47732  8exp8mod9  47737  ackval2  48671  ackval2012  48680