Theorem 2t1e2 12320

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

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   · cmul 11049  2c2 12217

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 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-mulcom 11108  ax-mulass 11110  ax-distr 11111  ax-1rid 11114  ax-cnre 11117

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225

This theorem is referenced by:  decbin2  12766  expubnd  14119  01sqrexlem7  15190  trirecip  15805  bpoly3  16000  fsumcube  16002  ege2le3  16032  cos2tsin  16123  cos2bnd  16132  odd2np1  16287  opoe  16309  flodddiv4  16361  2mulprm  16639  pythagtriplem4  16766  2503lem2  17084  2503lem3  17085  4001lem4  17090  4001prm  17091  htpycc  24912  pco1  24948  pcohtpylem  24952  pcopt  24955  pcorevlem  24959  ovolunlem1a  25430  cos2pi  26418  coskpi  26465  dcubic2  26787  dcubic  26789  basellem3  27026  chtublem  27155  bcp1ctr  27223  bclbnd  27224  bposlem1  27228  bposlem2  27229  bposlem5  27232  2lgslem3d1  27347  2sqreultlem  27391  2sqreunnltlem  27394  chebbnd1lem1  27413  chebbnd1lem3  27415  chebbnd1  27416  frgrregord013  30374  ex-ind-dvds  30440  wrdt2ind  32925  knoppndvlem12  36504  heiborlem6  37803  3lexlogpow5ineq1  42035  aks4d1p1  42057  2np3bcnp1  42125  2ap1caineq  42126  flt4lem7  42640  jm2.23  42978  sumnnodd  45621  wallispilem4  46059  wallispi2lem1  46062  wallispi2lem2  46063  wallispi2  46064  stirlinglem11  46075  dirkertrigeqlem1  46089  fouriersw  46222  fmtnorec4  47543  lighneallem2  47600  lighneallem3  47601  3exp4mod41  47610  opoeALTV  47677  fppr2odd  47725  8exp8mod9  47730  ackval2  48664  ackval2012  48673