Theorem 2t1e2 12518

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7430  1c1 11214   · cmul 11218  2c2 12410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-mulcl 11275  ax-mulcom 11277  ax-mulass 11279  ax-distr 11280  ax-1rid 11283  ax-cnre 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555  df-ov 7433  df-2 12418

This theorem is used by:  decbin2  12975  expubnd  14334  01sqrexlem7  15430  trirecip  16047  bpoly3  16239  fsumcube  16241  ege2le3  16271  cos2tsin  16362  cos2bnd  16371  odd2np1  16526  opoe  16548  flodddiv4  16600  2mulprm  16883  pythagtriplem4  17012  2503lem2  17331  2503lem3  17332  4001lem4  17337  4001prm  17338  htpycc  25316  pco1  25351  pcohtpylem  25355  pcopt  25358  pcorevlem  25362  ovolunlem1a  25832  cos2pi  26820  coskpi  26866  dcubic2  27187  dcubic  27189  basellem3  27425  chtublem  27553  bcp1ctr  27621  bclbnd  27622  bposlem1  27626  bposlem2  27627  bposlem5  27630  2lgslem3d1  27745  2sqreultlem  27789  2sqreunnltlem  27792  chebbnd1lem1  27811  chebbnd1lem3  27813  chebbnd1  27814  frgrregord013  31011  ex-ind-dvds  31077  wrdt2ind  33572  knoppndvlem12  37519  heiborlem6  38893  3lexlogpow5ineq1  43247  aks4d1p1  43269  2np3bcnp1  43337  2ap1caineq  43338  jm2.23  44146  sumnnodd  46784  wallispilem4  47220  wallispi2lem1  47223  wallispi2lem2  47224  wallispi2  47225  stirlinglem11  47236  dirkertrigeqlem1  47250  fouriersw  47383  goldratval  48078  fmtnorec4  48776  lighneallem2  48833  lighneallem3  48834  3exp4mod41  48843  opoeALTV  48923  fppr2odd  48971  8exp8mod9  48976  ackval2  49936  ackval2012  49945