Theorem 2p1e3 12313

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

Syntax hints:   = wceq 1548  (class class class)co 7360  1c1 11034   + caddc 11036  2c2 12231  3c3 12232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-3 12240

This theorem is referenced by:  1p2e3  12314  1p2e3ALT  12315  halfthird  12393  halfpm6th  12394  cnm2m1cnm3  12425  6t5e30  12746  7t5e35  12751  8t4e32  12756  9t4e36  12763  decbin3  12781  fz0to3un2pr  13578  fz0to4untppr  13579  fz0to5un2tp  13580  fzo0to42pr  13703  m1modge3gt1  13875  fac3  14237  hash3  14363  hashtplei  14441  hashtpg  14442  hash3tpexb  14451  s3len  14851  repsw3  14908  bpoly3  16018  bpoly4  16019  nn0o1gt2  16345  flodddiv4  16379  ge2nprmge4  16666  3exp3  17057  13prm  17081  37prm  17086  43prm  17087  83prm  17088  139prm  17089  163prm  17090  317prm  17091  631prm  17092  1259lem1  17096  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  1259prm  17101  2503lem2  17103  2503prm  17105  4001lem1  17106  4001lem2  17107  4001lem4  17109  4001prm  17110  mcubic  26833  log2ublem3  26934  log2ub  26935  birthday  26940  chtub  27197  2lgsoddprmlem3c  27397  istrkg3ld  28551  usgr2wlkspthlem2  29848  elwwlks2ons3im  30044  usgrwwlks2on  30048  umgrwwlks2on  30049  elwwlks2  30059  elwspths2spth  30060  clwwlknonex2lem1  30199  clwwlknonex2lem2  30200  3wlkdlem5  30255  3wlkdlem10  30261  upgr3v3e3cycl  30272  upgr4cycl4dv4e  30277  konigsberglem1  30344  konigsberglem2  30345  konigsberglem3  30346  numclwlk1  30463  frgrregord013  30487  ex-hash  30545  threehalves  32997  evl1deg2  33672  ply1dg3rt0irred  33679  cos9thpiminplylem1  33978  cos9thpiminplylem2  33979  cos9thpiminplylem5  33982  lmat22det  34018  fib3  34599  prodfzo03  34799  hgt750lemd  34844  hgt750lem  34847  hgt750lem2  34848  aks4d1p1p2  42570  aks4d1p1p7  42574  aks4d1p1  42576  2np3bcnp1  42644  aks6d1c7lem1  42680  3cubeslem3l  43150  3cubeslem3r  43151  jm2.23  43456  resqrtvalex  44104  lt3addmuld  45763  wallispilem4  46525  wallispi2lem1  46528  stirlinglem11  46541  sin3t  47348  sin5tlem4  47353  m1modnep2mod  47835  minusmodnep2tmod  47836  modm1nep2  47851  2timesltsqm1  47856  fmtno0  48032  fmtno5lem4  48048  fmtno4prmfac  48064  fmtno4nprmfac193  48066  139prmALT  48088  31prm  48089  m7prm  48092  lighneallem4a  48100  41prothprmlem2  48110  ppivalnnnprm  48120  2exp340mod341  48238  sbgoldbalt  48286  bgoldbtbndlem1  48310  tgoldbachlt  48321  cycl3grtrilem  48451  gpg5order  48565  gpg3kgrtriexlem2  48589  gpg5gricstgr3  48595  gpgprismgr4cycllem10  48609  pgnbgreunbgrlem2lem2  48620  pgrpgt2nabl  48871  ackval2  49187  ackval3  49188  ackval0012  49194  ackval3012  49197