Theorem 2t1e2 12398

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

Syntax hints:   = wceq 1570  (class class class)co 7410  1c1 11096   · cmul 11100  2c2 12290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-mulcom 11159  ax-mulass 11161  ax-distr 11162  ax-1rid 11165  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298

This theorem is referenced by:  decbin2  12854  expubnd  14210  01sqrexlem7  15295  trirecip  15913  bpoly3  16107  fsumcube  16109  ege2le3  16139  cos2tsin  16230  cos2bnd  16239  odd2np1  16394  opoe  16416  flodddiv4  16468  2mulprm  16746  pythagtriplem4  16874  2503lem2  17193  2503lem3  17194  4001lem4  17199  4001prm  17200  htpycc  25139  pco1  25174  pcohtpylem  25178  pcopt  25181  pcorevlem  25185  ovolunlem1a  25655  cos2pi  26641  coskpi  26688  dcubic2  27009  dcubic  27011  basellem3  27247  chtublem  27375  bcp1ctr  27443  bclbnd  27444  bposlem1  27448  bposlem2  27449  bposlem5  27452  2lgslem3d1  27567  2sqreultlem  27611  2sqreunnltlem  27614  chebbnd1lem1  27633  chebbnd1lem3  27635  chebbnd1  27636  frgrregord013  30746  ex-ind-dvds  30812  wrdt2ind  33273  knoppndvlem12  37132  heiborlem6  38487  3lexlogpow5ineq1  42841  aks4d1p1  42863  2np3bcnp1  42931  2ap1caineq  42932  flt4lem7  43411  jm2.23  43743  sumnnodd  46366  wallispilem4  46802  wallispi2lem1  46805  wallispi2lem2  46806  wallispi2  46807  stirlinglem11  46818  dirkertrigeqlem1  46832  fouriersw  46965  fmtnorec4  48321  lighneallem2  48378  lighneallem3  48379  3exp4mod41  48388  opoeALTV  48468  fppr2odd  48516  8exp8mod9  48521  ackval2  49482  ackval2012  49491