MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2t1e2 Structured version   Unicode version

Theorem 2t1e2 10574
Description: 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
2t1e2  |-  ( 2  x.  1 )  =  2

Proof of Theorem 2t1e2
StepHypRef Expression
1 2cn 10496 . 2  |-  2  e.  CC
21mulid1i 9492 1  |-  ( 2  x.  1 )  =  2
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370  (class class class)co 6193   1c1 9387    x. cmul 9391   2c2 10475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-resscn 9443  ax-1cn 9444  ax-icn 9445  ax-addcl 9446  ax-addrcl 9447  ax-mulcl 9448  ax-mulrcl 9449  ax-mulcom 9450  ax-mulass 9452  ax-distr 9453  ax-i2m1 9454  ax-1ne0 9455  ax-1rid 9456  ax-rrecex 9458  ax-cnre 9459
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-iota 5482  df-fv 5527  df-ov 6196  df-2 10484
This theorem is referenced by:  decbin2  10963  expubnd  12034  sqrlem7  12849  trirecip  13436  ege2le3  13486  cos2tsin  13574  cos2bnd  13583  odd2np1  13703  opoe  13989  pythagtriplem4  13997  2503lem2  14273  4001lem4  14279  htpycc  20677  pco1  20712  pcohtpylem  20716  pcopt  20719  pcorevlem  20723  ovolunlem1a  21104  cos2pi  22064  coskpi  22108  dcubic1lem  22364  dcubic2  22365  dcubic  22367  mcubic  22368  basellem3  22546  chtublem  22676  bcp1ctr  22744  bclbnd  22745  bposlem1  22749  bposlem2  22750  bposlem5  22753  chebbnd1lem1  22844  chebbnd1lem3  22846  chebbnd1  22847  konigsberg  23753  frgraregord013  30852
  Copyright terms: Public domain W3C validator