Theorem 2p1e3 12115

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

Syntax hints:   = wceq 1539  (class class class)co 7275  1c1 10872   + caddc 10874  2c2 12028  3c3 12029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-3 12037

This theorem is referenced by:  1p2e3  12116  1p2e3ALT  12117  cnm2m1cnm3  12226  6t5e30  12544  7t5e35  12549  8t4e32  12554  9t4e36  12561  decbin3  12579  halfthird  12580  fz0to3un2pr  13358  fzo0to42pr  13474  m1modge3gt1  13638  fac3  13994  hash3  14121  hashtplei  14198  hashtpg  14199  s3len  14607  repsw3  14664  bpoly3  15768  bpoly4  15769  nn0o1gt2  16090  flodddiv4  16122  ge2nprmge4  16406  3exp3  16793  13prm  16817  37prm  16822  43prm  16823  83prm  16824  139prm  16825  163prm  16826  317prm  16827  631prm  16828  1259lem1  16832  1259lem2  16833  1259lem3  16834  1259lem4  16835  1259lem5  16836  1259prm  16837  2503lem2  16839  2503prm  16841  4001lem1  16842  4001lem2  16843  4001lem4  16845  4001prm  16846  mcubic  25997  log2ublem3  26098  log2ub  26099  birthday  26104  chtub  26360  2lgsoddprmlem3c  26560  istrkg3ld  26822  usgr2wlkspthlem2  28126  elwwlks2ons3im  28319  umgrwwlks2on  28322  elwwlks2  28331  elwspths2spth  28332  clwwlknonex2lem1  28471  clwwlknonex2lem2  28472  3wlkdlem5  28527  3wlkdlem10  28533  upgr3v3e3cycl  28544  upgr4cycl4dv4e  28549  konigsberglem1  28616  konigsberglem2  28617  konigsberglem3  28618  numclwlk1  28735  frgrregord013  28759  ex-hash  28817  threehalves  31189  lmat22det  31772  fib3  32370  prodfzo03  32583  hgt750lemd  32628  hgt750lem  32631  hgt750lem2  32632  aks4d1p1p2  40078  aks4d1p1p7  40082  aks4d1p1  40084  2np3bcnp1  40100  3cubeslem3l  40508  3cubeslem3r  40509  jm2.23  40818  resqrtvalex  41253  lt3addmuld  42840  wallispilem4  43609  wallispi2lem1  43612  stirlinglem11  43625  fmtno0  44992  fmtno5lem4  45008  fmtno4prmfac  45024  fmtno4nprmfac193  45026  139prmALT  45048  31prm  45049  m7prm  45052  lighneallem4a  45060  41prothprmlem2  45070  2exp340mod341  45185  sbgoldbalt  45233  bgoldbtbndlem1  45257  tgoldbachlt  45268  pgrpgt2nabl  45702  ackval2  46028  ackval3  46029  ackval0012  46035  ackval3012  46038