Theorem 1p1e2 12479

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7430  1c1 11214   + caddc 11216  2c2 12410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-2 12418

This theorem is used by:  2m1e1OLD  12481  1p2e3  12498  add1p1  12610  sub1m1  12611  nn0n0n1ge2  12687  3halfnz  12791  10p10e20  12927  5t4e20  12934  6t4e24  12938  7t3e21  12942  8t3e24  12948  9t3e27  12955  fz12pr  13728  fz0to3un2pr  13776  fzo13pr  13897  fzo1to4tp  13902  fldiv4p1lem1div2  13988  m1modge3gt1  14074  fac2  14436  hash2  14562  hashprlei  14626  ccat2s1len  14785  ccat2s1p2  14792  s2len  15054  repsw2  15118  swrd2lsw  15120  2swrd2eqwrdeq  15121  nn0o1gt2  16566  3lcm2e6woprm  16805  ge2nprmge4  16892  2exp8  17281  2exp11  17282  2exp16  17283  prmlem0  17298  prmlem2  17313  37prm  17314  43prm  17315  83prm  17316  317prm  17319  631prm  17320  1259lem1  17324  1259lem2  17325  1259lem4  17327  1259lem5  17328  2503lem1  17330  2503lem2  17331  2503lem3  17332  2503prm  17333  4001lem2  17335  4001lem3  17336  4001lem4  17337  m2detleiblem2  22958  logbleb  27126  logblt  27127  log2ublem3  27291  log2ub  27292  1sgm2ppw  27542  2sqb  27774  2sq2  27775  rplogsumlem2  27827  flt0  27984  tgldimor  28980  1loopgrvd2  30099  2wlklem  30261  pthdlem1  30367  pthdlem2  30369  wwlksnextwrd  30501  wwlksnextproplem3  30515  2wlkdlem5  30533  2wlkdlem10  30539  rusgrnumwwlkl1  30575  clwlkclwwlklem2a4  30603  clwlkclwwlklem2a  30604  clwwlkext2edg  30662  wwlksext2clwwlk  30663  clwlknf1oclwwlknlem1  30687  3wlkdlem5  30779  3wlkdlem10  30785  upgr3v3e3cycl  30796  upgr4cycl4dv4e  30801  konigsberglem1  30868  konigsberglem2  30869  konigsberglem3  30870  numclwlk2lem2f  30993  ex-exp  31066  1nei  33385  psgnfzto1st  33722  cyc3fv2  33755  archirngz  33806  archiabllem2c  33812  cos9thpiminplylem1  34470  lmat22e12  34507  lmat22e21  34508  lmat22e22  34509  madjusmdetlem4  34518  fiblem  35086  fibp1  35089  fib2  35090  fib3  35091  ballotlem2  35177  ballotlemfc0  35181  ballotlemfcc  35182  signstfveq0  35262  chtvalz  35314  hgt750lem  35336  hgt750lem2  35337  subfacp1lem5  36073  dnibndlem13  37489  knoppndvlem12  37522  420gcd8e4  43202  3exp7  43249  3lexlogpow5ineq1  43250  aks4d1p1  43272  2np3bcnp1  43340  sn-0ne2  43603  fltnltalem  43819  rabren3dioph  43968  pellfundgt1  44036  areaquad  44364  resqrtvalex  44791  imsqrtvalex  44792  trclfvdecomr  44874  xralrple2  46511  sumnnodd  46787  itgsin0pilem1  47105  itgsinexp  47110  stoweidlem14  47169  stoweidlem26  47181  wallispilem3  47222  stirlinglem6  47234  stirlinglem11  47239  dirkertrigeqlem1  47253  sqwvfourb  47384  fourierswlem  47385  addmodne  48565  fmtno5lem1  48783  fmtno5lem4  48786  257prm  48791  fmtnoprmfac1lem  48794  fmtnofac1  48800  127prm  48829  m11nprm  48831  lighneallem2  48836  proththd  48844  opoeALTV  48926  1oddALTV  48933  nnsum3primes4  49031  nnsum3primesgbe  49035  nnsum4primesodd  49039  nnsum4primesoddALTV  49040  bgoldbtbndlem1  49048  grtriclwlk3  49188  cycl3grtrilem  49189  gpgprismgr4cycllem10  49347  oddinmgm  49417  fldivexpfllog2  49822  blen2  49842  ackval1  49938  ackval0012  49946  crosspdotsumlem  51184  crosspaltd  51186  crossp3d  51187  veronesevrowd  51199  veroquadgsumlem  51203