Theorem 1p1e2 12364

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

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11101   + caddc 11103  2c2 12295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-2 12303

This theorem is referenced by:  2m1e1OLD  12366  1p2e3  12383  add1p1  12495  sub1m1  12496  nn0n0n1ge2  12572  3halfnz  12675  10p10e20  12811  5t4e20  12818  6t4e24  12822  7t3e21  12826  8t3e24  12832  9t3e27  12839  fz12pr  13609  fz0to3un2pr  13657  fzo13pr  13778  fzo1to4tp  13783  fldiv4p1lem1div2  13868  m1modge3gt1  13954  fac2  14315  hash2  14441  hashprlei  14505  ccat2s1len  14661  ccat2s1p2  14668  s2len  14926  repsw2  14987  swrd2lsw  14989  2swrd2eqwrdeq  14990  nn0o1gt2  16439  3lcm2e6woprm  16673  ge2nprmge4  16760  2exp8  17148  2exp11  17149  2exp16  17150  prmlem0  17165  prmlem2  17180  37prm  17181  43prm  17182  83prm  17183  317prm  17186  631prm  17187  1259lem1  17191  1259lem2  17192  1259lem4  17194  1259lem5  17195  2503lem1  17197  2503lem2  17198  2503lem3  17199  2503prm  17200  4001lem2  17202  4001lem3  17203  4001lem4  17204  m2detleiblem2  22754  logbleb  26914  logblt  26915  log2ublem3  27079  log2ub  27080  1sgm2ppw  27330  2sqb  27562  2sq2  27563  rplogsumlem2  27615  tgldimor  28737  1loopgrvd2  29794  2wlklem  29956  pthdlem1  30056  pthdlem2  30058  wwlksnextwrd  30187  wwlksnextproplem3  30201  2wlkdlem5  30219  2wlkdlem10  30225  rusgrnumwwlkl1  30261  clwlkclwwlklem2a4  30289  clwlkclwwlklem2a  30290  clwwlkext2edg  30348  wwlksext2clwwlk  30349  clwlknf1oclwwlknlem1  30373  3wlkdlem5  30455  3wlkdlem10  30461  upgr3v3e3cycl  30472  upgr4cycl4dv4e  30477  konigsberglem1  30544  konigsberglem2  30545  konigsberglem3  30546  numclwlk2lem2f  30669  ex-exp  30742  1nei  33023  psgnfzto1st  33366  cyc3fv2  33399  archirngz  33450  archiabllem2c  33456  cos9thpiminplylem1  34117  lmat22e12  34154  lmat22e21  34155  lmat22e22  34156  madjusmdetlem4  34165  fiblem  34733  fibp1  34736  fib2  34737  fib3  34738  ballotlem2  34824  ballotlemfc0  34828  ballotlemfcc  34829  signstfveq0  34909  chtvalz  34961  hgt750lem  34983  hgt750lem2  34984  subfacp1lem5  35609  dnibndlem13  37002  knoppndvlem12  37035  420gcd8e4  42697  3exp7  42744  3lexlogpow5ineq1  42745  aks4d1p1  42767  2np3bcnp1  42835  sn-0ne2  43091  flt0  43295  fltnltalem  43320  rabren3dioph  43468  pellfundgt1  43536  areaquad  43869  resqrtvalex  44297  imsqrtvalex  44298  trclfvdecomr  44380  xralrple2  45996  sumnnodd  46272  itgsin0pilem1  46590  itgsinexp  46595  stoweidlem14  46654  stoweidlem26  46666  wallispilem3  46707  stirlinglem6  46719  stirlinglem11  46724  dirkertrigeqlem1  46738  sqwvfourb  46869  fourierswlem  46870  addmodne  48010  fmtno5lem1  48228  fmtno5lem4  48231  257prm  48236  fmtnoprmfac1lem  48239  fmtnofac1  48245  127prm  48274  m11nprm  48276  lighneallem2  48281  proththd  48289  opoeALTV  48371  1oddALTV  48378  nnsum3primes4  48476  nnsum3primesgbe  48480  nnsum4primesodd  48484  nnsum4primesoddALTV  48485  bgoldbtbndlem1  48493  grtriclwlk3  48633  cycl3grtrilem  48634  gpgprismgr4cycllem10  48792  oddinmgm  48863  fldivexpfllog2  49264  blen2  49284  ackval1  49380  ackval0012  49388