Theorem 1p1e2 12418

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 12356	. 2 ⊢ 2 = (1 + 1)
2	1	eqcomi 2749	1 ⊢ (1 + 1) = 2

Syntax hints:   = wceq 1537  (class class class)co 7448  1c1 11185   + caddc 11187  2c2 12348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-2 12356

This theorem is referenced by:  2m1e1  12419  1p2e3  12436  add1p1  12544  sub1m1  12545  nn0n0n1ge2  12620  3halfnz  12722  10p10e20  12853  5t4e20  12860  6t4e24  12864  7t3e21  12868  8t3e24  12874  9t3e27  12881  fz12pr  13641  fz0to3un2pr  13686  fzo13pr  13800  fzo1to4tp  13804  fldiv4p1lem1div2  13886  m1modge3gt1  13969  fac2  14328  hash2  14454  hashprlei  14517  ccat2s1len  14671  ccat2s1p2  14678  s2len  14938  repsw2  14999  swrd2lsw  15001  2swrd2eqwrdeq  15002  nn0o1gt2  16429  3lcm2e6woprm  16662  ge2nprmge4  16748  2exp8  17136  2exp11  17137  2exp16  17138  prmlem0  17153  prmlem2  17167  37prm  17168  43prm  17169  83prm  17170  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem4  17181  1259lem5  17182  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem2  17189  4001lem3  17190  4001lem4  17191  m2detleiblem2  22655  logbleb  26844  logblt  26845  log2ublem3  27009  log2ub  27010  1sgm2ppw  27262  2sqb  27494  2sq2  27495  rplogsumlem2  27547  tgldimor  28528  1loopgrvd2  29539  2wlklem  29703  pthdlem1  29802  pthdlem2  29804  wwlksnextwrd  29930  wwlksnextproplem3  29944  2wlkdlem5  29962  2wlkdlem10  29968  rusgrnumwwlkl1  30001  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwwlkext2edg  30088  wwlksext2clwwlk  30089  clwlknf1oclwwlknlem1  30113  3wlkdlem5  30195  3wlkdlem10  30201  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  numclwlk2lem2f  30409  ex-exp  30482  1nei  32750  psgnfzto1st  33098  cyc3fv2  33131  archirngz  33169  archiabllem2c  33175  lmat22e12  33765  lmat22e21  33766  lmat22e22  33767  madjusmdetlem4  33776  fiblem  34363  fibp1  34366  fib2  34367  fib3  34368  ballotlem2  34453  ballotlemfc0  34457  ballotlemfcc  34458  signstfveq0  34554  chtvalz  34606  hgt750lem  34628  hgt750lem2  34629  subfacp1lem5  35152  dnibndlem13  36456  knoppndvlem12  36489  420gcd8e4  41963  3exp7  42010  3lexlogpow5ineq1  42011  aks4d1p1  42033  2np3bcnp1  42101  sn-0ne2  42382  flt0  42592  fltnltalem  42617  rabren3dioph  42771  pellfundgt1  42839  areaquad  43177  resqrtvalex  43607  imsqrtvalex  43608  trclfvdecomr  43690  xralrple2  45269  sumnnodd  45551  itgsin0pilem1  45871  itgsinexp  45876  stoweidlem14  45935  stoweidlem26  45947  wallispilem3  45988  stirlinglem6  46000  stirlinglem11  46005  dirkertrigeqlem1  46019  sqwvfourb  46150  fourierswlem  46151  fmtno5lem1  47427  fmtno5lem4  47430  257prm  47435  fmtnoprmfac1lem  47438  fmtnofac1  47444  127prm  47473  m11nprm  47475  lighneallem2  47480  proththd  47488  opoeALTV  47557  1oddALTV  47564  nnsum3primes4  47662  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  bgoldbtbndlem1  47679  grtriclwlk3  47796  oddinmgm  47898  fldivexpfllog2  48299  blen2  48319  ackval1  48415  ackval0012  48423