Theorem 2p1e3 12397

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11116   + caddc 11118  2c2 12310  3c3 12311

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

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

This theorem is used by:  1p2e3  12398  1p2e3ALT  12399  halfthird  12480  halfpm6th  12481  cnm2m1cnm3  12512  6t5e30  12839  7t5e35  12844  8t4e32  12849  9t4e36  12856  decbin3  12876  fz0to3un2pr  13674  fz0to4untppr  13675  fz0to5un2tp  13676  fzo0to42pr  13799  m1modge3gt1  13972  fac3  14334  hash3  14460  hashtplei  14539  hashtpg  14540  hash3tpexb  14549  s3len  14955  repsw3  15012  bpoly3  16134  bpoly4  16135  nn0o1gt2  16461  flodddiv4  16495  ge2nprmge4  16782  3exp3  17173  13prm  17198  37prm  17203  43prm  17204  83prm  17205  139prm  17206  163prm  17207  317prm  17208  631prm  17209  1259lem1  17213  1259lem2  17214  1259lem3  17215  1259lem4  17216  1259lem5  17217  1259prm  17218  2503lem2  17220  2503prm  17222  4001lem1  17223  4001lem2  17224  4001lem4  17226  4001prm  17227  mcubic  27063  log2ublem3  27164  log2ub  27165  birthday  27170  chtub  27427  2lgsoddprmlem3c  27627  istrkg3ld  28781  usgr2wlkspthlem2  30171  elwwlks2ons3im  30370  usgrwwlks2on  30374  umgrwwlks2on  30375  elwwlks2  30385  elwspths2spth  30386  clwwlknonex2lem1  30525  clwwlknonex2lem2  30526  3wlkdlem5  30585  3wlkdlem10  30591  upgr3v3e3cycl  30602  upgr4cycl4dv4e  30607  konigsberglem1  30674  konigsberglem2  30675  konigsberglem3  30676  numclwlk1  30793  frgrregord013  30817  ex-hash  30875  threehalves  33304  evl1deg2  33931  ply1dg3rt0irred  33938  cos9thpiminplylem1  34236  cos9thpiminplylem2  34237  cos9thpiminplylem5  34240  lmat22det  34276  fib3  34858  prodfzo03  35055  hgt750lemd  35100  hgt750lem  35103  hgt750lem2  35104  aks4d1p1p2  42895  aks4d1p1p7  42899  aks4d1p1  42901  2np3bcnp1  42969  aks6d1c7lem1  43005  3cubeslem3l  43475  3cubeslem3r  43476  jm2.23  43781  resqrtvalex  44429  lt3addmuld  46078  wallispilem4  46840  wallispi2lem1  46843  stirlinglem11  46856  sin3t  47666  sin5tlem4  47671  m1modnep2mod  48153  minusmodnep2tmod  48154  modm1nep2  48169  2timesltsqm1  48174  fmtno0  48350  fmtno5lem4  48366  fmtno4prmfac  48382  fmtno4nprmfac193  48384  139prmALT  48406  31prm  48407  m7prm  48410  lighneallem4a  48418  41prothprmlem2  48428  ppivalnnnprm  48438  2exp340mod341  48556  sbgoldbalt  48604  bgoldbtbndlem1  48628  tgoldbachlt  48639  cycl3grtrilem  48769  gpg5order  48883  gpg3kgrtriexlem2  48907  gpg5gricstgr3  48913  gpgprismgr4cycllem10  48927  pgnbgreunbgrlem2lem2  48938  pgrpgt2nabl  49203  ackval2  49519  ackval3  49520  ackval0012  49526  ackval3012  49529