Theorem 1p1e2 12368

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7410  1c1 11105   + caddc 11107  2c2 12299

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-2 12307

This theorem is used by:  2m1e1OLD  12370  1p2e3  12387  add1p1  12499  sub1m1  12500  nn0n0n1ge2  12576  3halfnz  12679  10p10e20  12815  5t4e20  12822  6t4e24  12826  7t3e21  12830  8t3e24  12836  9t3e27  12843  fz12pr  13614  fz0to3un2pr  13662  fzo13pr  13783  fzo1to4tp  13788  fldiv4p1lem1div2  13873  m1modge3gt1  13959  fac2  14320  hash2  14446  hashprlei  14510  ccat2s1len  14666  ccat2s1p2  14673  s2len  14931  repsw2  14992  swrd2lsw  14994  2swrd2eqwrdeq  14995  nn0o1gt2  16443  3lcm2e6woprm  16677  ge2nprmge4  16764  2exp8  17152  2exp11  17153  2exp16  17154  prmlem0  17169  prmlem2  17184  37prm  17185  43prm  17186  83prm  17187  317prm  17190  631prm  17191  1259lem1  17195  1259lem2  17196  1259lem4  17198  1259lem5  17199  2503lem1  17201  2503lem2  17202  2503lem3  17203  2503prm  17204  4001lem2  17206  4001lem3  17207  4001lem4  17208  m2detleiblem2  22794  logbleb  26957  logblt  26958  log2ublem3  27122  log2ub  27123  1sgm2ppw  27373  2sqb  27605  2sq2  27606  rplogsumlem2  27658  tgldimor  28780  1loopgrvd2  29862  2wlklem  30024  pthdlem1  30124  pthdlem2  30126  wwlksnextwrd  30255  wwlksnextproplem3  30269  2wlkdlem5  30287  2wlkdlem10  30293  rusgrnumwwlkl1  30329  clwlkclwwlklem2a4  30357  clwlkclwwlklem2a  30358  clwwlkext2edg  30416  wwlksext2clwwlk  30417  clwlknf1oclwwlknlem1  30441  3wlkdlem5  30523  3wlkdlem10  30529  upgr3v3e3cycl  30540  upgr4cycl4dv4e  30545  konigsberglem1  30612  konigsberglem2  30613  konigsberglem3  30614  numclwlk2lem2f  30737  ex-exp  30810  1nei  33091  psgnfzto1st  33434  cyc3fv2  33467  archirngz  33518  archiabllem2c  33524  cos9thpiminplylem1  34181  lmat22e12  34218  lmat22e21  34219  lmat22e22  34220  madjusmdetlem4  34229  fiblem  34797  fibp1  34800  fib2  34801  fib3  34802  ballotlem2  34888  ballotlemfc0  34892  ballotlemfcc  34893  signstfveq0  34973  chtvalz  35025  hgt750lem  35047  hgt750lem2  35048  subfacp1lem5  35684  dnibndlem13  37107  knoppndvlem12  37140  420gcd8e4  42801  3exp7  42848  3lexlogpow5ineq1  42849  aks4d1p1  42871  2np3bcnp1  42939  sn-0ne2  43195  flt0  43397  fltnltalem  43422  rabren3dioph  43570  pellfundgt1  43638  areaquad  43971  resqrtvalex  44399  imsqrtvalex  44400  trclfvdecomr  44482  xralrple2  46098  sumnnodd  46374  itgsin0pilem1  46692  itgsinexp  46697  stoweidlem14  46756  stoweidlem26  46768  wallispilem3  46809  stirlinglem6  46821  stirlinglem11  46826  dirkertrigeqlem1  46840  sqwvfourb  46971  fourierswlem  46972  addmodne  48115  fmtno5lem1  48333  fmtno5lem4  48336  257prm  48341  fmtnoprmfac1lem  48344  fmtnofac1  48350  127prm  48379  m11nprm  48381  lighneallem2  48386  proththd  48394  opoeALTV  48476  1oddALTV  48483  nnsum3primes4  48581  nnsum3primesgbe  48585  nnsum4primesodd  48589  nnsum4primesoddALTV  48590  bgoldbtbndlem1  48598  grtriclwlk3  48738  cycl3grtrilem  48739  gpgprismgr4cycllem10  48897  oddinmgm  48968  fldivexpfllog2  49373  blen2  49393  ackval1  49489  ackval0012  49497  crosspdotsumi  50673  crosspalti  50675  crossp3i  50676