Theorem 1p1e2 11011

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

Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  2c2 10947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-2 10956

This theorem is referenced by:  2m1e1  11012  add1p1  11160  sub1m1  11161  nn0n0n1ge2  11235  3halfnz  11332  10p10e20  11504  10p10e20OLD  11505  5t4e20  11513  5t4e20OLD  11514  6t4e24  11519  7t3e21  11525  8t3e24  11531  9t3e27  11540  fz0to3un2pr  12310  fzo13pr  12419  fzo1to4tp  12423  fldiv4p1lem1div2  12498  m1modge3gt1  12579  fac2  12928  hash2  13054  hashprlei  13107  ccat2s1len  13253  ccat2s1p2  13258  s2len  13484  repsw2  13541  swrd2lsw  13543  2swrd2eqwrdeq  13544  nn0o1gt2  14935  3lcm2e6woprm  15166  2exp8  15634  2exp16  15635  prmlem0  15650  prmlem2  15665  37prm  15666  43prm  15667  83prm  15668  317prm  15671  631prm  15672  1259lem1  15676  1259lem2  15677  1259lem4  15679  1259lem5  15680  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem2  15687  4001lem3  15688  4001lem4  15689  m2detleiblem2  20253  iblcnlem1  23360  logbleb  24321  logblt  24322  log2ublem3  24475  log2ub  24476  1sgm2ppw  24725  2sqb  24957  rplogsumlem2  24974  tgldimor  25197  wlkntrllem2  26090  2wlklem  26094  wlkdvspthlem  26137  3v3e3cycl1  26172  constr3trllem5  26182  constr3pthlem1  26183  constr3pthlem3  26185  wwlkextwrd  26256  wwlkextproplem3  26271  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwwlkext2edg  26330  wwlkext2clwwlk  26331  nbhashuvtx1  26442  rusgranumwlkl1  26474  numclwlk1lem2fo  26622  numclwlk2lem2f  26630  ex-exp  26699  archirngz  29074  archiabllem2c  29080  psgnfzto1st  29186  lmat22e12  29213  lmat22e21  29214  lmat22e22  29215  madjusmdetlem4  29224  fiblem  29787  fibp1  29790  fib2  29791  fib3  29792  ballotlem2  29877  ballotlemfc0  29881  ballotlemfcc  29882  signstfveq0  29980  subfacp1lem5  30420  dnibndlem13  31650  knoppndvlem12  31684  rabren3dioph  36397  pellfundgt1  36465  areaquad  36821  trclfvdecomr  37039  xralrple2  38511  sumnnodd  38697  itgsin0pilem1  38841  itgsinexp  38846  stoweidlem14  38907  stoweidlem26  38919  wallispilem3  38960  stirlinglem6  38972  stirlinglem11  38977  dirkertrigeqlem1  38991  sqwvfourb  39122  fourierswlem  39123  fmtno5lem1  40003  fmtno5lem4  40006  257prm  40011  fmtnoprmfac1lem  40014  fmtnofac1  40020  127prm  40053  2exp11  40055  m11nprm  40056  lighneallem2  40061  proththd  40069  opoeALTV  40132  1oddALTV  40139  nnsum3primes4  40204  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  bgoldbtbndlem1  40221  1loopgrvd2  40718  2Wlklem  40875  usgr2wlkneq  40962  usgr2trlncl  40966  pthdlem1  40972  pthdlem2  40974  wwlksnextwrd  41103  wwlksnextproplem3  41117  21wlkdlem5  41136  21wlkdlem10  41142  rusgrnumwwlkl1  41172  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwwlksext2edg  41230  wwlksext2clwwlk  41231  31wlkdlem5  41330  31wlkdlem10  41336  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424  av-numclwlk1lem2fo  41525  av-numclwlk2lem2f  41533  oddinmgm  41605  fldivexpfllog2  42157  blen2  42177