Theorem 1p1e2 12248

Description: 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)

Assertion

Ref	Expression
1p1e2	⊢ (1 + 1) = 2

Proof of Theorem 1p1e2

Step	Hyp	Ref	Expression
1		df-2 12191	. 2 ⊢ 2 = (1 + 1)
2	1	eqcomi 2738	1 ⊢ (1 + 1) = 2

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012  2c2 12183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-2 12191

This theorem is referenced by:  2m1e1  12249  1p2e3  12266  add1p1  12375  sub1m1  12376  nn0n0n1ge2  12452  3halfnz  12555  10p10e20  12686  5t4e20  12693  6t4e24  12697  7t3e21  12701  8t3e24  12707  9t3e27  12714  fz12pr  13484  fz0to3un2pr  13532  fzo13pr  13652  fzo1to4tp  13657  fldiv4p1lem1div2  13739  m1modge3gt1  13825  fac2  14186  hash2  14312  hashprlei  14375  ccat2s1len  14530  ccat2s1p2  14537  s2len  14796  repsw2  14857  swrd2lsw  14859  2swrd2eqwrdeq  14860  nn0o1gt2  16292  3lcm2e6woprm  16526  ge2nprmge4  16612  2exp8  17000  2exp11  17001  2exp16  17002  prmlem0  17017  prmlem2  17031  37prm  17032  43prm  17033  83prm  17034  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem2  17053  4001lem3  17054  4001lem4  17055  m2detleiblem2  22513  logbleb  26691  logblt  26692  log2ublem3  26856  log2ub  26857  1sgm2ppw  27109  2sqb  27341  2sq2  27342  rplogsumlem2  27394  tgldimor  28447  1loopgrvd2  29449  2wlklem  29611  pthdlem1  29711  pthdlem2  29713  wwlksnextwrd  29842  wwlksnextproplem3  29856  2wlkdlem5  29874  2wlkdlem10  29880  rusgrnumwwlkl1  29913  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwwlkext2edg  30000  wwlksext2clwwlk  30001  clwlknf1oclwwlknlem1  30025  3wlkdlem5  30107  3wlkdlem10  30113  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  konigsberglem1  30196  konigsberglem2  30197  konigsberglem3  30198  numclwlk2lem2f  30321  ex-exp  30394  1nei  32681  psgnfzto1st  33048  cyc3fv2  33081  archirngz  33132  archiabllem2c  33138  cos9thpiminplylem1  33755  lmat22e12  33792  lmat22e21  33793  lmat22e22  33794  madjusmdetlem4  33803  fiblem  34372  fibp1  34375  fib2  34376  fib3  34377  ballotlem2  34463  ballotlemfc0  34467  ballotlemfcc  34468  signstfveq0  34551  chtvalz  34603  hgt750lem  34625  hgt750lem2  34626  subfacp1lem5  35167  dnibndlem13  36474  knoppndvlem12  36507  420gcd8e4  41989  3exp7  42036  3lexlogpow5ineq1  42037  aks4d1p1  42059  2np3bcnp1  42127  sn-0ne2  42389  flt0  42620  fltnltalem  42645  rabren3dioph  42798  pellfundgt1  42866  areaquad  43199  resqrtvalex  43628  imsqrtvalex  43629  trclfvdecomr  43711  xralrple2  45344  sumnnodd  45621  itgsin0pilem1  45941  itgsinexp  45946  stoweidlem14  46005  stoweidlem26  46017  wallispilem3  46058  stirlinglem6  46070  stirlinglem11  46075  dirkertrigeqlem1  46089  sqwvfourb  46220  fourierswlem  46221  addmodne  47338  fmtno5lem1  47547  fmtno5lem4  47550  257prm  47555  fmtnoprmfac1lem  47558  fmtnofac1  47564  127prm  47593  m11nprm  47595  lighneallem2  47600  proththd  47608  opoeALTV  47677  1oddALTV  47684  nnsum3primes4  47782  nnsum3primesgbe  47786  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  bgoldbtbndlem1  47799  grtriclwlk3  47939  cycl3grtrilem  47940  gpgprismgr4cycllem10  48098  oddinmgm  48169  fldivexpfllog2  48560  blen2  48580  ackval1  48676  ackval0012  48684