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

Theorem 1p1e2 10096
Description: One plus one equals two. (Contributed by NM, 1-Apr-2008.)
Assertion
Ref Expression
1p1e2  |-  ( 1  +  1 )  =  2

Proof of Theorem 1p1e2
StepHypRef Expression
1 df-2 10060 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2442 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff set class
Syntax hints:    = wceq 1653  (class class class)co 6083   1c1 8993    + caddc 8995   2c2 10051
This theorem is referenced by:  2m1e1  10097  nn0n0n1ge2  10282  10p10e20  10454  5t4e20  10459  6t4e24  10463  7t3e21  10467  8t3e24  10473  9t3e27  10480  fac2  11574  hash2  11676  hashprlei  11688  s2len  11853  2exp8  13425  2exp16  13426  prmlem0  13430  prmlem2  13444  37prm  13445  43prm  13446  83prm  13447  317prm  13450  631prm  13451  1259lem1  13452  1259lem2  13453  1259lem4  13455  1259lem5  13456  2503lem1  13458  2503lem2  13459  2503lem3  13460  2503prm  13461  4001lem2  13463  4001lem3  13464  4001lem4  13465  iblcnlem1  19681  log2ublem3  20790  log2ub  20791  1sgm2ppw  20986  2sqb  21164  rplogsumlem2  21181  wlkntrllem2  21562  2wlklem  21566  wlkdvspthlem  21609  usgrcyclnl2  21630  3v3e3cycl1  21633  constr3trllem5  21643  constr3pthlem1  21644  constr3pthlem3  21646  4cycl4v4e  21655  4cycl4dv4e  21657  logblt  24408  ballotlem2  24748  ballotlemfc0  24752  ballotlemfcc  24753  subfacp1lem5  24872  rabren3dioph  26878  itgsin0pilem1  27722  itgsinexp  27727  stoweidlem14  27741  stoweidlem26  27753  wallispilem3  27794  stirlinglem6  27806  stirlinglem11  27811  swrdtrcfvl  28267  usgra2pthspth  28307  usgra2wlkspthlem1  28308  usgra2pthlem1  28312  usgra2pth  28313
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431  df-2 10060
  Copyright terms: Public domain W3C validator