Theorem 1p1e2 12388

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

Syntax hints:   = wceq 1536  (class class class)co 7430  1c1 11153   + caddc 11155  2c2 12318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-2 12326

This theorem is referenced by:  2m1e1  12389  1p2e3  12406  add1p1  12514  sub1m1  12515  nn0n0n1ge2  12591  3halfnz  12694  10p10e20  12825  5t4e20  12832  6t4e24  12836  7t3e21  12840  8t3e24  12846  9t3e27  12853  fz12pr  13617  fz0to3un2pr  13665  fzo13pr  13784  fzo1to4tp  13789  fldiv4p1lem1div2  13871  m1modge3gt1  13955  fac2  14314  hash2  14440  hashprlei  14503  ccat2s1len  14657  ccat2s1p2  14664  s2len  14924  repsw2  14985  swrd2lsw  14987  2swrd2eqwrdeq  14988  nn0o1gt2  16414  3lcm2e6woprm  16648  ge2nprmge4  16734  2exp8  17122  2exp11  17123  2exp16  17124  prmlem0  17139  prmlem2  17153  37prm  17154  43prm  17155  83prm  17156  317prm  17159  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem4  17167  1259lem5  17168  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem2  17175  4001lem3  17176  4001lem4  17177  m2detleiblem2  22649  logbleb  26840  logblt  26841  log2ublem3  27005  log2ub  27006  1sgm2ppw  27258  2sqb  27490  2sq2  27491  rplogsumlem2  27543  tgldimor  28524  1loopgrvd2  29535  2wlklem  29699  pthdlem1  29798  pthdlem2  29800  wwlksnextwrd  29926  wwlksnextproplem3  29940  2wlkdlem5  29958  2wlkdlem10  29964  rusgrnumwwlkl1  29997  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwwlkext2edg  30084  wwlksext2clwwlk  30085  clwlknf1oclwwlknlem1  30109  3wlkdlem5  30191  3wlkdlem10  30197  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  numclwlk2lem2f  30405  ex-exp  30478  1nei  32753  psgnfzto1st  33107  cyc3fv2  33140  archirngz  33178  archiabllem2c  33184  lmat22e12  33779  lmat22e21  33780  lmat22e22  33781  madjusmdetlem4  33790  fiblem  34379  fibp1  34382  fib2  34383  fib3  34384  ballotlem2  34469  ballotlemfc0  34473  ballotlemfcc  34474  signstfveq0  34570  chtvalz  34622  hgt750lem  34644  hgt750lem2  34645  subfacp1lem5  35168  dnibndlem13  36472  knoppndvlem12  36505  420gcd8e4  41987  3exp7  42034  3lexlogpow5ineq1  42035  aks4d1p1  42057  2np3bcnp1  42125  sn-0ne2  42412  flt0  42623  fltnltalem  42648  rabren3dioph  42802  pellfundgt1  42870  areaquad  43204  resqrtvalex  43634  imsqrtvalex  43635  trclfvdecomr  43717  xralrple2  45303  sumnnodd  45585  itgsin0pilem1  45905  itgsinexp  45910  stoweidlem14  45969  stoweidlem26  45981  wallispilem3  46022  stirlinglem6  46034  stirlinglem11  46039  dirkertrigeqlem1  46053  sqwvfourb  46184  fourierswlem  46185  addmodne  47283  fmtno5lem1  47477  fmtno5lem4  47480  257prm  47485  fmtnoprmfac1lem  47488  fmtnofac1  47494  127prm  47523  m11nprm  47525  lighneallem2  47530  proththd  47538  opoeALTV  47607  1oddALTV  47614  nnsum3primes4  47712  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  bgoldbtbndlem1  47729  grtriclwlk3  47849  oddinmgm  48018  fldivexpfllog2  48414  blen2  48434  ackval1  48530  ackval0012  48538