Theorem 1p1e2 12391

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7414  1c1 11128   + caddc 11130  2c2 12322

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-2 12330

This theorem is used by:  2m1e1OLD  12393  1p2e3  12410  add1p1  12522  sub1m1  12523  nn0n0n1ge2  12599  3halfnz  12703  10p10e20  12839  5t4e20  12846  6t4e24  12850  7t3e21  12854  8t3e24  12860  9t3e27  12867  fz12pr  13639  fz0to3un2pr  13687  fzo13pr  13808  fzo1to4tp  13813  fldiv4p1lem1div2  13899  m1modge3gt1  13985  fac2  14346  hash2  14472  hashprlei  14536  ccat2s1len  14694  ccat2s1p2  14701  s2len  14963  repsw2  15026  swrd2lsw  15028  2swrd2eqwrdeq  15029  nn0o1gt2  16474  3lcm2e6woprm  16708  ge2nprmge4  16795  2exp8  17183  2exp11  17184  2exp16  17185  prmlem0  17200  prmlem2  17215  37prm  17216  43prm  17217  83prm  17218  317prm  17221  631prm  17222  1259lem1  17226  1259lem2  17227  1259lem4  17229  1259lem5  17230  2503lem1  17232  2503lem2  17233  2503lem3  17234  2503prm  17235  4001lem2  17237  4001lem3  17238  4001lem4  17239  m2detleiblem2  22853  logbleb  27023  logblt  27024  log2ublem3  27188  log2ub  27189  1sgm2ppw  27439  2sqb  27671  2sq2  27672  rplogsumlem2  27724  tgldimor  28847  1loopgrvd2  29966  2wlklem  30128  pthdlem1  30234  pthdlem2  30236  wwlksnextwrd  30368  wwlksnextproplem3  30382  2wlkdlem5  30400  2wlkdlem10  30406  rusgrnumwwlkl1  30442  clwlkclwwlklem2a4  30470  clwlkclwwlklem2a  30471  clwwlkext2edg  30529  wwlksext2clwwlk  30530  clwlknf1oclwwlknlem1  30554  3wlkdlem5  30646  3wlkdlem10  30652  upgr3v3e3cycl  30663  upgr4cycl4dv4e  30668  konigsberglem1  30735  konigsberglem2  30736  konigsberglem3  30737  numclwlk2lem2f  30860  ex-exp  30933  1nei  33211  psgnfzto1st  33548  cyc3fv2  33581  archirngz  33632  archiabllem2c  33638  cos9thpiminplylem1  34295  lmat22e12  34332  lmat22e21  34333  lmat22e22  34334  madjusmdetlem4  34343  fiblem  34912  fibp1  34915  fib2  34916  fib3  34917  ballotlem2  35003  ballotlemfc0  35007  ballotlemfcc  35008  signstfveq0  35088  chtvalz  35140  hgt750lem  35162  hgt750lem2  35163  subfacp1lem5  35766  dnibndlem13  37190  knoppndvlem12  37223  420gcd8e4  42875  3exp7  42922  3lexlogpow5ineq1  42923  aks4d1p1  42945  2np3bcnp1  43013  sn-0ne2  43284  flt0  43486  fltnltalem  43511  rabren3dioph  43659  pellfundgt1  43727  areaquad  44060  resqrtvalex  44488  imsqrtvalex  44489  trclfvdecomr  44571  xralrple2  46187  sumnnodd  46463  itgsin0pilem1  46781  itgsinexp  46786  stoweidlem14  46845  stoweidlem26  46857  wallispilem3  46898  stirlinglem6  46910  stirlinglem11  46915  dirkertrigeqlem1  46929  sqwvfourb  47060  fourierswlem  47061  addmodne  48241  fmtno5lem1  48459  fmtno5lem4  48462  257prm  48467  fmtnoprmfac1lem  48470  fmtnofac1  48476  127prm  48505  m11nprm  48507  lighneallem2  48512  proththd  48520  opoeALTV  48602  1oddALTV  48609  nnsum3primes4  48707  nnsum3primesgbe  48711  nnsum4primesodd  48715  nnsum4primesoddALTV  48716  bgoldbtbndlem1  48724  grtriclwlk3  48864  cycl3grtrilem  48865  gpgprismgr4cycllem10  49023  oddinmgm  49093  fldivexpfllog2  49498  blen2  49518  ackval1  49614  ackval0012  49622  crosspdotsumlem  50800  crosspaltd  50802  crossp3d  50803  veronesevrowd  50815  veroquadgsumlem  50819