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

Theorem 1p1e2 12211
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 12149 . 2 2 = (1 + 1)
21eqcomi 2746 1 (1 + 1) = 2
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  (class class class)co 7349  1c1 10985   + caddc 10987  2c2 12141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2729  df-2 12149
This theorem is referenced by:  2m1e1  12212  1p2e3  12229  add1p1  12337  sub1m1  12338  nn0n0n1ge2  12413  3halfnz  12512  10p10e20  12645  5t4e20  12652  6t4e24  12656  7t3e21  12660  8t3e24  12666  9t3e27  12673  fz12pr  13426  fz0to3un2pr  13471  fzo13pr  13584  fzo1to4tp  13588  fldiv4p1lem1div2  13668  m1modge3gt1  13751  fac2  14106  hash2  14232  hashprlei  14294  ccat2s1len  14438  ccat2s1p2  14445  s2len  14709  repsw2  14770  swrd2lsw  14772  2swrd2eqwrdeq  14773  nn0o1gt2  16197  3lcm2e6woprm  16425  ge2nprmge4  16511  2exp8  16895  2exp11  16896  2exp16  16897  prmlem0  16912  prmlem2  16926  37prm  16927  43prm  16928  83prm  16929  317prm  16932  631prm  16933  1259lem1  16937  1259lem2  16938  1259lem4  16940  1259lem5  16941  2503lem1  16943  2503lem2  16944  2503lem3  16945  2503prm  16946  4001lem2  16948  4001lem3  16949  4001lem4  16950  m2detleiblem2  21899  logbleb  26055  logblt  26056  log2ublem3  26220  log2ub  26221  1sgm2ppw  26470  2sqb  26702  2sq2  26703  rplogsumlem2  26755  tgldimor  27242  1loopgrvd2  28249  2wlklem  28413  pthdlem1  28512  pthdlem2  28514  wwlksnextwrd  28640  wwlksnextproplem3  28654  2wlkdlem5  28672  2wlkdlem10  28678  rusgrnumwwlkl1  28711  clwlkclwwlklem2a4  28739  clwlkclwwlklem2a  28740  clwwlkext2edg  28798  wwlksext2clwwlk  28799  clwlknf1oclwwlknlem1  28823  3wlkdlem5  28905  3wlkdlem10  28911  upgr3v3e3cycl  28922  upgr4cycl4dv4e  28927  konigsberglem1  28994  konigsberglem2  28995  konigsberglem3  28996  numclwlk2lem2f  29119  ex-exp  29192  1nei  31447  psgnfzto1st  31748  cyc3fv2  31781  archirngz  31819  archiabllem2c  31825  lmat22e12  32173  lmat22e21  32174  lmat22e22  32175  madjusmdetlem4  32184  fiblem  32771  fibp1  32774  fib2  32775  fib3  32776  ballotlem2  32861  ballotlemfc0  32865  ballotlemfcc  32866  signstfveq0  32962  chtvalz  33015  hgt750lem  33037  hgt750lem2  33038  subfacp1lem5  33551  dnibndlem13  34848  knoppndvlem12  34881  420gcd8e4  40358  3exp7  40405  3lexlogpow5ineq1  40406  aks4d1p1  40428  2np3bcnp1  40447  sn-0ne2  40743  flt0  40840  fltnltalem  40865  rabren3dioph  41003  pellfundgt1  41071  areaquad  41415  resqrtvalex  41679  imsqrtvalex  41680  trclfvdecomr  41762  xralrple2  43345  sumnnodd  43624  itgsin0pilem1  43944  itgsinexp  43949  stoweidlem14  44008  stoweidlem26  44020  wallispilem3  44061  stirlinglem6  44073  stirlinglem11  44078  dirkertrigeqlem1  44092  sqwvfourb  44223  fourierswlem  44224  fmtno5lem1  45494  fmtno5lem4  45497  257prm  45502  fmtnoprmfac1lem  45505  fmtnofac1  45511  127prm  45540  m11nprm  45542  lighneallem2  45547  proththd  45555  opoeALTV  45624  1oddALTV  45631  nnsum3primes4  45729  nnsum3primesgbe  45733  nnsum4primesodd  45737  nnsum4primesoddALTV  45738  bgoldbtbndlem1  45746  oddinmgm  45858  fldivexpfllog2  46400  blen2  46420  ackval1  46516  ackval0012  46524
  Copyright terms: Public domain W3C validator