Theorem 2p1e3 12524

Description: 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
2p1e3	⊢ (2 + 1) = 3

Proof of Theorem 2p1e3

Step	Hyp	Ref	Expression
1		df-3 12446	. 2 ⊢ 3 = (2 + 1)
2	1	eqcomi 2772	1 ⊢ (2 + 1) = 3

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451  1c1 11240   + caddc 11242  2c2 12437  3c3 12438

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-3 12446

This theorem is used by:  1p2e3  12525  1p2e3ALT  12526  halfthird  12607  halfpm6th  12608  cnm2m1cnm3  12639  6t5e30  12966  7t5e35  12971  8t4e32  12976  9t4e36  12983  decbin3  13003  fz0to3un2pr  13803  fz0to4untppr  13804  fz0to5un2tp  13805  fzo0to42pr  13928  m1modge3gt1  14101  fac3  14465  hash3  14591  hashtplei  14670  hashtpg  14671  hash3tpexb  14680  s3len  15088  repsw3  15147  bpoly3  16268  bpoly4  16269  nn0o1gt2  16595  flodddiv4  16629  ge2nprmge4  16921  3exp3  17313  13prm  17338  37prm  17343  43prm  17344  83prm  17345  139prm  17346  163prm  17347  317prm  17348  631prm  17349  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  1259prm  17358  2503lem2  17360  2503prm  17362  4001lem1  17363  4001lem2  17364  4001lem4  17366  4001prm  17367  mcubic  27232  log2ublem3  27333  log2ub  27334  birthday  27339  chtub  27596  2lgsoddprmlem3c  27796  fltoprmgt3  28053  istrkg3ld  28980  usgr2wlkspthlem2  30401  elwwlks2ons3im  30600  usgrwwlks2on  30604  umgrwwlks2on  30605  elwwlks2  30615  elwspths2spth  30616  clwwlknonex2lem1  30755  clwwlknonex2lem2  30756  3wlkdlem5  30821  3wlkdlem10  30827  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  konigsberglem1  30910  konigsberglem2  30911  konigsberglem3  30912  numclwlk1  31029  frgrregord013  31053  ex-hash  31111  threehalves  33577  evl1deg2  34212  ply1dg3rt0irred  34219  cos9thpiminplylem1  34525  cos9thpiminplylem2  34526  cos9thpiminplylem5  34529  lmat22det  34565  fib3  35146  prodfzo03  35343  hgt750lemd  35388  hgt750lem  35391  hgt750lem2  35392  aks4d1p1p2  43386  aks4d1p1p7  43390  aks4d1p1  43392  2np3bcnp1  43460  aks6d1c7lem1  43496  2p3e5  43582  3cubeslem3l  43962  3cubeslem3r  43963  jm2.23  44269  resqrtvalex  44906  lt3addmuld  46590  wallispilem4  47351  wallispi2lem1  47354  stirlinglem11  47367  sin3t  48190  sin5tlem4  48195  m1modnep2mod  48701  minusmodnep2tmod  48702  modm1nep2  48717  2timesltsqm1  48722  fmtno0  48898  fmtno5lem4  48914  fmtno4prmfac  48930  fmtno4nprmfac193  48932  139prmALT  48954  31prm  48955  m7prm  48958  lighneallem4a  48966  41prothprmlem2  48976  ppivalnnnprm  48986  2exp340mod341  49104  sbgoldbalt  49152  bgoldbtbndlem1  49176  tgoldbachlt  49187  cycl3grtrilem  49317  gpg5order  49431  gpg3kgrtriexlem2  49455  gpg5gricstgr3  49461  gpgprismgr4cycllem10  49475  pgnbgreunbgrlem2lem2  49486  pgrpgt2nabl  49809  ackval2  50125  ackval3  50126  ackval0012  50132  ackval3012  50135  veronesevrowd  51407  veroquadgsumlem  51411