Theorem 1p1e2 12309

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

Syntax hints:   = wceq 1541  (class class class)co 7384  1c1 11083   + caddc 11085  2c2 12239

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-2 12247

This theorem is referenced by:  2m1e1  12310  1p2e3  12327  add1p1  12435  sub1m1  12436  nn0n0n1ge2  12511  3halfnz  12613  10p10e20  12744  5t4e20  12751  6t4e24  12755  7t3e21  12759  8t3e24  12765  9t3e27  12772  fz12pr  13530  fz0to3un2pr  13575  fzo13pr  13688  fzo1to4tp  13692  fldiv4p1lem1div2  13772  m1modge3gt1  13855  fac2  14211  hash2  14337  hashprlei  14401  ccat2s1len  14545  ccat2s1p2  14552  s2len  14812  repsw2  14873  swrd2lsw  14875  2swrd2eqwrdeq  14876  nn0o1gt2  16296  3lcm2e6woprm  16524  ge2nprmge4  16610  2exp8  16994  2exp11  16995  2exp16  16996  prmlem0  17011  prmlem2  17025  37prm  17026  43prm  17027  83prm  17028  317prm  17031  631prm  17032  1259lem1  17036  1259lem2  17037  1259lem4  17039  1259lem5  17040  2503lem1  17042  2503lem2  17043  2503lem3  17044  2503prm  17045  4001lem2  17047  4001lem3  17048  4001lem4  17049  m2detleiblem2  22036  logbleb  26192  logblt  26193  log2ublem3  26357  log2ub  26358  1sgm2ppw  26607  2sqb  26839  2sq2  26840  rplogsumlem2  26892  tgldimor  27548  1loopgrvd2  28555  2wlklem  28719  pthdlem1  28818  pthdlem2  28820  wwlksnextwrd  28946  wwlksnextproplem3  28960  2wlkdlem5  28978  2wlkdlem10  28984  rusgrnumwwlkl1  29017  clwlkclwwlklem2a4  29045  clwlkclwwlklem2a  29046  clwwlkext2edg  29104  wwlksext2clwwlk  29105  clwlknf1oclwwlknlem1  29129  3wlkdlem5  29211  3wlkdlem10  29217  upgr3v3e3cycl  29228  upgr4cycl4dv4e  29233  konigsberglem1  29300  konigsberglem2  29301  konigsberglem3  29302  numclwlk2lem2f  29425  ex-exp  29498  1nei  31762  psgnfzto1st  32065  cyc3fv2  32098  archirngz  32136  archiabllem2c  32142  lmat22e12  32530  lmat22e21  32531  lmat22e22  32532  madjusmdetlem4  32541  fiblem  33128  fibp1  33131  fib2  33132  fib3  33133  ballotlem2  33218  ballotlemfc0  33222  ballotlemfcc  33223  signstfveq0  33319  chtvalz  33372  hgt750lem  33394  hgt750lem2  33395  subfacp1lem5  33906  dnibndlem13  35070  knoppndvlem12  35103  420gcd8e4  40576  3exp7  40623  3lexlogpow5ineq1  40624  aks4d1p1  40646  2np3bcnp1  40665  sn-0ne2  40973  flt0  41073  fltnltalem  41098  rabren3dioph  41236  pellfundgt1  41304  areaquad  41648  resqrtvalex  42079  imsqrtvalex  42080  trclfvdecomr  42162  xralrple2  43749  sumnnodd  44031  itgsin0pilem1  44351  itgsinexp  44356  stoweidlem14  44415  stoweidlem26  44427  wallispilem3  44468  stirlinglem6  44480  stirlinglem11  44485  dirkertrigeqlem1  44499  sqwvfourb  44630  fourierswlem  44631  fmtno5lem1  45905  fmtno5lem4  45908  257prm  45913  fmtnoprmfac1lem  45916  fmtnofac1  45922  127prm  45951  m11nprm  45953  lighneallem2  45958  proththd  45966  opoeALTV  46035  1oddALTV  46042  nnsum3primes4  46140  nnsum3primesgbe  46144  nnsum4primesodd  46148  nnsum4primesoddALTV  46149  bgoldbtbndlem1  46157  oddinmgm  46269  fldivexpfllog2  46811  blen2  46831  ackval1  46927  ackval0012  46935