Theorem 2p1e3 12330

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 12257	. 2 ⊢ 3 = (2 + 1)
2	1	eqcomi 2739	1 ⊢ (2 + 1) = 3

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   + caddc 11078  2c2 12248  3c3 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-3 12257

This theorem is referenced by:  1p2e3  12331  1p2e3ALT  12332  halfthird  12410  halfpm6th  12411  cnm2m1cnm3  12442  6t5e30  12763  7t5e35  12768  8t4e32  12773  9t4e36  12780  decbin3  12798  fz0to3un2pr  13597  fz0to4untppr  13598  fz0to5un2tp  13599  fzo0to42pr  13721  m1modge3gt1  13890  fac3  14252  hash3  14378  hashtplei  14456  hashtpg  14457  hash3tpexb  14466  s3len  14867  repsw3  14924  bpoly3  16031  bpoly4  16032  nn0o1gt2  16358  flodddiv4  16392  ge2nprmge4  16678  3exp3  17069  13prm  17093  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem2  17115  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem4  17121  4001prm  17122  mcubic  26764  log2ublem3  26865  log2ub  26866  birthday  26871  chtub  27130  2lgsoddprmlem3c  27330  istrkg3ld  28395  usgr2wlkspthlem2  29695  elwwlks2ons3im  29891  umgrwwlks2on  29894  elwwlks2  29903  elwspths2spth  29904  clwwlknonex2lem1  30043  clwwlknonex2lem2  30044  3wlkdlem5  30099  3wlkdlem10  30105  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  numclwlk1  30307  frgrregord013  30331  ex-hash  30389  threehalves  32842  evl1deg2  33553  ply1dg3rt0irred  33558  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem5  33783  lmat22det  33819  fib3  34401  prodfzo03  34601  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  aks4d1p1p2  42065  aks4d1p1p7  42069  aks4d1p1  42071  2np3bcnp1  42139  aks6d1c7lem1  42175  3cubeslem3l  42681  3cubeslem3r  42682  jm2.23  42992  resqrtvalex  43641  lt3addmuld  45306  wallispilem4  46073  wallispi2lem1  46076  stirlinglem11  46089  m1modnep2mod  47357  minusmodnep2tmod  47358  modm1nep2  47373  fmtno0  47545  fmtno5lem4  47561  fmtno4prmfac  47577  fmtno4nprmfac193  47579  139prmALT  47601  31prm  47602  m7prm  47605  lighneallem4a  47613  41prothprmlem2  47623  2exp340mod341  47738  sbgoldbalt  47786  bgoldbtbndlem1  47810  tgoldbachlt  47821  cycl3grtrilem  47949  gpg5order  48055  gpg3kgrtriexlem2  48079  gpg5gricstgr3  48085  gpgprismgr4cycllem10  48098  pgnbgreunbgrlem2lem2  48109  pgrpgt2nabl  48358  ackval2  48675  ackval3  48676  ackval0012  48682  ackval3012  48685