Theorem 2p1e3 12375

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

Syntax hints:   = wceq 1539  (class class class)co 7400  1c1 11123   + caddc 11125  2c2 12288  3c3 12289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-3 12297

This theorem is referenced by:  1p2e3  12376  1p2e3ALT  12377  halfthird  12455  halfpm6th  12456  cnm2m1cnm3  12487  6t5e30  12808  7t5e35  12813  8t4e32  12818  9t4e36  12825  decbin3  12843  fz0to3un2pr  13636  fz0to4untppr  13637  fz0to5un2tp  13638  fzo0to42pr  13759  m1modge3gt1  13926  fac3  14288  hash3  14414  hashtplei  14492  hashtpg  14493  hash3tpexb  14502  s3len  14902  repsw3  14959  bpoly3  16063  bpoly4  16064  nn0o1gt2  16387  flodddiv4  16421  ge2nprmge4  16707  3exp3  17098  13prm  17122  37prm  17127  43prm  17128  83prm  17129  139prm  17130  163prm  17131  317prm  17132  631prm  17133  1259lem1  17137  1259lem2  17138  1259lem3  17139  1259lem4  17140  1259lem5  17141  1259prm  17142  2503lem2  17144  2503prm  17146  4001lem1  17147  4001lem2  17148  4001lem4  17150  4001prm  17151  mcubic  26795  log2ublem3  26896  log2ub  26897  birthday  26902  chtub  27161  2lgsoddprmlem3c  27361  istrkg3ld  28374  usgr2wlkspthlem2  29674  elwwlks2ons3im  29870  umgrwwlks2on  29873  elwwlks2  29882  elwspths2spth  29883  clwwlknonex2lem1  30022  clwwlknonex2lem2  30023  3wlkdlem5  30078  3wlkdlem10  30084  upgr3v3e3cycl  30095  upgr4cycl4dv4e  30100  konigsberglem1  30167  konigsberglem2  30168  konigsberglem3  30169  numclwlk1  30286  frgrregord013  30310  ex-hash  30368  threehalves  32826  evl1deg2  33526  ply1dg3rt0irred  33531  cos9thpiminplylem1  33751  cos9thpiminplylem2  33752  lmat22det  33782  fib3  34364  prodfzo03  34564  hgt750lemd  34609  hgt750lem  34612  hgt750lem2  34613  aks4d1p1p2  42012  aks4d1p1p7  42016  aks4d1p1  42018  2np3bcnp1  42086  aks6d1c7lem1  42122  3cubeslem3l  42641  3cubeslem3r  42642  jm2.23  42952  resqrtvalex  43601  lt3addmuld  45264  wallispilem4  46033  wallispi2lem1  46036  stirlinglem11  46049  m1modnep2mod  47307  minusmodnep2tmod  47308  fmtno0  47480  fmtno5lem4  47496  fmtno4prmfac  47512  fmtno4nprmfac193  47514  139prmALT  47536  31prm  47537  m7prm  47540  lighneallem4a  47548  41prothprmlem2  47558  2exp340mod341  47673  sbgoldbalt  47721  bgoldbtbndlem1  47745  tgoldbachlt  47756  cycl3grtrilem  47866  gpg5order  47967  gpg3kgrtriexlem2  47993  gpg5gricstgr3  47999  pgrpgt2nabl  48235  ackval2  48556  ackval3  48557  ackval0012  48563  ackval3012  48566