Theorem 2t1e2 12351

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

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   · cmul 11080  2c2 12248

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 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256

This theorem is referenced by:  decbin2  12797  expubnd  14150  01sqrexlem7  15221  trirecip  15836  bpoly3  16031  fsumcube  16033  ege2le3  16063  cos2tsin  16154  cos2bnd  16163  odd2np1  16318  opoe  16340  flodddiv4  16392  2mulprm  16670  pythagtriplem4  16797  2503lem2  17115  2503lem3  17116  4001lem4  17121  4001prm  17122  htpycc  24886  pco1  24922  pcohtpylem  24926  pcopt  24929  pcorevlem  24933  ovolunlem1a  25404  cos2pi  26392  coskpi  26439  dcubic2  26761  dcubic  26763  basellem3  27000  chtublem  27129  bcp1ctr  27197  bclbnd  27198  bposlem1  27202  bposlem2  27203  bposlem5  27206  2lgslem3d1  27321  2sqreultlem  27365  2sqreunnltlem  27368  chebbnd1lem1  27387  chebbnd1lem3  27389  chebbnd1  27390  frgrregord013  30331  ex-ind-dvds  30397  wrdt2ind  32882  knoppndvlem12  36518  heiborlem6  37817  3lexlogpow5ineq1  42049  aks4d1p1  42071  2np3bcnp1  42139  2ap1caineq  42140  flt4lem7  42654  jm2.23  42992  sumnnodd  45635  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem11  46089  dirkertrigeqlem1  46103  fouriersw  46236  fmtnorec4  47554  lighneallem2  47611  lighneallem3  47612  3exp4mod41  47621  opoeALTV  47688  fppr2odd  47736  8exp8mod9  47741  ackval2  48675  ackval2012  48684