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

Theorem 1p1e2 12212
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 12150 . 2 2 = (1 + 1)
21eqcomi 2747 1 (1 + 1) = 2
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7350  1c1 10986   + caddc 10988  2c2 12142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2730  df-2 12150
This theorem is referenced by:  2m1e1  12213  1p2e3  12230  add1p1  12338  sub1m1  12339  nn0n0n1ge2  12414  3halfnz  12513  10p10e20  12646  5t4e20  12653  6t4e24  12657  7t3e21  12661  8t3e24  12667  9t3e27  12674  fz12pr  13427  fz0to3un2pr  13472  fzo13pr  13585  fzo1to4tp  13589  fldiv4p1lem1div2  13669  m1modge3gt1  13752  fac2  14107  hash2  14233  hashprlei  14295  ccat2s1len  14439  ccat2s1p2  14446  s2len  14710  repsw2  14771  swrd2lsw  14773  2swrd2eqwrdeq  14774  nn0o1gt2  16198  3lcm2e6woprm  16426  ge2nprmge4  16512  2exp8  16896  2exp11  16897  2exp16  16898  prmlem0  16913  prmlem2  16927  37prm  16928  43prm  16929  83prm  16930  317prm  16933  631prm  16934  1259lem1  16938  1259lem2  16939  1259lem4  16941  1259lem5  16942  2503lem1  16944  2503lem2  16945  2503lem3  16946  2503prm  16947  4001lem2  16949  4001lem3  16950  4001lem4  16951  m2detleiblem2  21899  logbleb  26055  logblt  26056  log2ublem3  26220  log2ub  26221  1sgm2ppw  26470  2sqb  26702  2sq2  26703  rplogsumlem2  26755  tgldimor  27230  1loopgrvd2  28237  2wlklem  28401  pthdlem1  28500  pthdlem2  28502  wwlksnextwrd  28628  wwlksnextproplem3  28642  2wlkdlem5  28660  2wlkdlem10  28666  rusgrnumwwlkl1  28699  clwlkclwwlklem2a4  28727  clwlkclwwlklem2a  28728  clwwlkext2edg  28786  wwlksext2clwwlk  28787  clwlknf1oclwwlknlem1  28811  3wlkdlem5  28893  3wlkdlem10  28899  upgr3v3e3cycl  28910  upgr4cycl4dv4e  28915  konigsberglem1  28982  konigsberglem2  28983  konigsberglem3  28984  numclwlk2lem2f  29107  ex-exp  29180  1nei  31435  psgnfzto1st  31736  cyc3fv2  31769  archirngz  31807  archiabllem2c  31813  lmat22e12  32161  lmat22e21  32162  lmat22e22  32163  madjusmdetlem4  32172  fiblem  32759  fibp1  32762  fib2  32763  fib3  32764  ballotlem2  32849  ballotlemfc0  32853  ballotlemfcc  32854  signstfveq0  32950  chtvalz  33003  hgt750lem  33025  hgt750lem2  33026  subfacp1lem5  33539  dnibndlem13  34839  knoppndvlem12  34872  420gcd8e4  40349  3exp7  40396  3lexlogpow5ineq1  40397  aks4d1p1  40419  2np3bcnp1  40438  sn-0ne2  40722  flt0  40809  fltnltalem  40834  rabren3dioph  40972  pellfundgt1  41040  areaquad  41384  resqrtvalex  41648  imsqrtvalex  41649  trclfvdecomr  41731  xralrple2  43302  sumnnodd  43581  itgsin0pilem1  43901  itgsinexp  43906  stoweidlem14  43965  stoweidlem26  43977  wallispilem3  44018  stirlinglem6  44030  stirlinglem11  44035  dirkertrigeqlem1  44049  sqwvfourb  44180  fourierswlem  44181  fmtno5lem1  45445  fmtno5lem4  45448  257prm  45453  fmtnoprmfac1lem  45456  fmtnofac1  45462  127prm  45491  m11nprm  45493  lighneallem2  45498  proththd  45506  opoeALTV  45575  1oddALTV  45582  nnsum3primes4  45680  nnsum3primesgbe  45684  nnsum4primesodd  45688  nnsum4primesoddALTV  45689  bgoldbtbndlem1  45697  oddinmgm  45809  fldivexpfllog2  46351  blen2  46371  ackval1  46467  ackval0012  46475
  Copyright terms: Public domain W3C validator