Theorem 2t1e2 12403

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

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11101   · cmul 11105  2c2 12295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-mulcl 11162  ax-mulcom 11164  ax-mulass 11166  ax-distr 11167  ax-1rid 11170  ax-cnre 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12303

This theorem is referenced by:  decbin2  12859  expubnd  14214  01sqrexlem7  15299  trirecip  15917  bpoly3  16112  fsumcube  16114  ege2le3  16144  cos2tsin  16235  cos2bnd  16244  odd2np1  16399  opoe  16421  flodddiv4  16473  2mulprm  16751  pythagtriplem4  16879  2503lem2  17198  2503lem3  17199  4001lem4  17204  4001prm  17205  htpycc  25108  pco1  25143  pcohtpylem  25147  pcopt  25150  pcorevlem  25154  ovolunlem1a  25624  cos2pi  26607  coskpi  26654  dcubic2  26975  dcubic  26977  basellem3  27213  chtublem  27341  bcp1ctr  27409  bclbnd  27410  bposlem1  27414  bposlem2  27415  bposlem5  27418  2lgslem3d1  27533  2sqreultlem  27577  2sqreunnltlem  27580  chebbnd1lem1  27599  chebbnd1lem3  27601  chebbnd1  27602  frgrregord013  30687  ex-ind-dvds  30753  wrdt2ind  33214  knoppndvlem12  37035  heiborlem6  38389  3lexlogpow5ineq1  42745  aks4d1p1  42767  2np3bcnp1  42835  2ap1caineq  42836  flt4lem7  43317  jm2.23  43649  sumnnodd  46272  wallispilem4  46708  wallispi2lem1  46711  wallispi2lem2  46712  wallispi2  46713  stirlinglem11  46724  dirkertrigeqlem1  46738  fouriersw  46871  fmtnorec4  48224  lighneallem2  48281  lighneallem3  48282  3exp4mod41  48291  opoeALTV  48371  fppr2odd  48419  8exp8mod9  48424  ackval2  49381  ackval2012  49390