Theorem 2p1e3 12489

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7422  1c1 11206   + caddc 11208  2c2 12402  3c3 12403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-3 12411

This theorem is used by:  1p2e3  12490  1p2e3ALT  12491  halfthird  12572  halfpm6th  12573  cnm2m1cnm3  12604  6t5e30  12931  7t5e35  12936  8t4e32  12941  9t4e36  12948  decbin3  12968  fz0to3un2pr  13768  fz0to4untppr  13769  fz0to5un2tp  13770  fzo0to42pr  13893  m1modge3gt1  14066  fac3  14429  hash3  14555  hashtplei  14634  hashtpg  14635  hash3tpexb  14644  s3len  15052  repsw3  15111  bpoly3  16231  bpoly4  16232  nn0o1gt2  16558  flodddiv4  16592  ge2nprmge4  16884  3exp3  17276  13prm  17301  37prm  17306  43prm  17307  83prm  17308  139prm  17309  163prm  17310  317prm  17311  631prm  17312  1259lem1  17316  1259lem2  17317  1259lem3  17318  1259lem4  17319  1259lem5  17320  1259prm  17321  2503lem2  17323  2503prm  17325  4001lem1  17326  4001lem2  17327  4001lem4  17329  4001prm  17330  mcubic  27182  log2ublem3  27283  log2ub  27284  birthday  27289  chtub  27546  2lgsoddprmlem3c  27746  fltoprmgt3  28003  istrkg3ld  28930  usgr2wlkspthlem2  30351  elwwlks2ons3im  30550  usgrwwlks2on  30554  umgrwwlks2on  30555  elwwlks2  30565  elwspths2spth  30566  clwwlknonex2lem1  30705  clwwlknonex2lem2  30706  3wlkdlem5  30771  3wlkdlem10  30777  upgr3v3e3cycl  30788  upgr4cycl4dv4e  30793  konigsberglem1  30860  konigsberglem2  30861  konigsberglem3  30862  numclwlk1  30979  frgrregord013  31003  ex-hash  31061  threehalves  33529  evl1deg2  34157  ply1dg3rt0irred  34164  cos9thpiminplylem1  34462  cos9thpiminplylem2  34463  cos9thpiminplylem5  34466  lmat22det  34502  fib3  35083  prodfzo03  35280  hgt750lemd  35325  hgt750lem  35328  hgt750lem2  35329  aks4d1p1p2  43227  aks4d1p1p7  43231  aks4d1p1  43233  2np3bcnp1  43301  aks6d1c7lem1  43337  2p3e5  43423  3cubeslem3l  43803  3cubeslem3r  43804  jm2.23  44110  resqrtvalex  44752  lt3addmuld  46424  wallispilem4  47185  wallispi2lem1  47188  stirlinglem11  47201  sin3t  48024  sin5tlem4  48029  m1modnep2mod  48535  minusmodnep2tmod  48536  modm1nep2  48551  2timesltsqm1  48556  fmtno0  48732  fmtno5lem4  48748  fmtno4prmfac  48764  fmtno4nprmfac193  48766  139prmALT  48788  31prm  48789  m7prm  48792  lighneallem4a  48800  41prothprmlem2  48810  ppivalnnnprm  48820  2exp340mod341  48938  sbgoldbalt  48986  bgoldbtbndlem1  49010  tgoldbachlt  49021  cycl3grtrilem  49151  gpg5order  49265  gpg3kgrtriexlem2  49289  gpg5gricstgr3  49295  gpgprismgr4cycllem10  49309  pgnbgreunbgrlem2lem2  49320  pgrpgt2nabl  49585  ackval2  49901  ackval3  49902  ackval0012  49908  ackval3012  49911  veronesevrowd  51161  veroquadgsumlem  51165