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

Theorem 1p1e2 10730
Description: 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
Assertion
Ref Expression
1p1e2  |-  ( 1  +  1 )  =  2

Proof of Theorem 1p1e2
StepHypRef Expression
1 df-2 10675 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2462 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff setvar class
Syntax hints:    = wceq 1446  (class class class)co 6295   1c1 9545    + caddc 9547   2c2 10666
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-cleq 2446  df-2 10675
This theorem is referenced by:  2m1e1  10731  add1p1  10869  sub1m1  10870  nn0n0n1ge2  10939  10p10e20  11128  5t4e20  11133  6t4e24  11137  7t3e21  11141  8t3e24  11147  9t3e27  11154  fzo13pr  12004  fac2  12472  hash2  12589  hashprlei  12636  ccat2s1len  12764  ccat2s1p2  12769  s2len  12990  repsw2  13037  swrd2lsw  13039  2swrd2eqwrdeq  13040  3lcm2e6woprm  14592  2exp8  15072  2exp16  15073  prmlem0  15089  prmlem2  15103  37prm  15104  43prm  15105  83prm  15106  317prm  15109  631prm  15110  1259lem1  15114  1259lem2  15115  1259lem4  15117  1259lem5  15118  2503lem1  15120  2503lem2  15121  2503lem3  15122  2503prm  15123  4001lem2  15125  4001lem3  15126  4001lem4  15127  m2detleiblem2  19665  iblcnlem1  22757  logbleb  23732  logblt  23733  log2ublem3  23886  log2ub  23887  1sgm2ppw  24140  2sqb  24318  rplogsumlem2  24335  tgldimor  24558  wlkntrllem2  25302  2wlklem  25306  wlkdvspthlem  25349  3v3e3cycl1  25384  constr3trllem5  25394  constr3pthlem1  25395  constr3pthlem3  25397  wwlkextwrd  25468  wwlkextproplem3  25483  clwlkisclwwlklem2a4  25524  clwlkisclwwlklem2a  25525  clwwlkext2edg  25542  wwlkext2clwwlk  25543  nbhashuvtx1  25655  rusgranumwlkl1  25687  numclwlk1lem2fo  25835  numclwlk2lem2f  25843  archirngz  28518  archiabllem2c  28524  psgnfzto1st  28630  lmat22e12  28657  lmat22e21  28658  lmat22e22  28659  madjusmdetlem4  28668  fiblem  29243  fibp1  29246  fib2  29247  fib3  29248  ballotlem2  29333  ballotlemfc0  29337  ballotlemfcc  29338  signstfveq0  29478  subfacp1lem5  29919  rabren3dioph  35670  areaquad  36113  trclfvdecomr  36332  xralrple2  37587  sumnnodd  37720  itgsin0pilem1  37836  itgsinexp  37841  stoweidlem14  37884  stoweidlem26  37896  wallispilem3  37939  stirlinglem6  37951  stirlinglem11  37956  dirkertrigeqlem1  37970  sqwvfourb  38103  fourierswlem  38104  opoeALTV  38822  1oddALTV  38829  nnsum3primes4  38893  nnsum3primesgbe  38897  nnsum4primesodd  38901  nnsum4primesoddALTV  38902  bgoldbtbndlem1  38910  proththd  38924  uspgrloopvd2  39567  2Wlklem  39671  21wlkdlem4  39760  oddinmgm  39919  3halfnz  40421  nn0o1gt2  40431  fldivexpfllog2  40480  blen2  40500
  Copyright terms: Public domain W3C validator