Theorem 2p1e3 11773

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

Syntax hints:   = wceq 1533  (class class class)co 7150  1c1 10532   + caddc 10534  2c2 11686  3c3 11687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-3 11695

This theorem is referenced by:  1p2e3  11774  1p2e3ALT  11775  cnm2m1cnm3  11884  6t5e30  12199  7t5e35  12204  8t4e32  12209  9t4e36  12216  decbin3  12234  halfthird  12235  fz0to3un2pr  13003  fzo0to42pr  13118  m1modge3gt1  13280  fac3  13634  hash3  13761  hashtplei  13836  hashtpg  13837  s3len  14250  repsw3  14307  bpoly3  15406  bpoly4  15407  nn0o1gt2  15726  flodddiv4  15758  ge2nprmge4  16039  3exp3  16419  13prm  16443  37prm  16448  43prm  16449  83prm  16450  139prm  16451  163prm  16452  317prm  16453  631prm  16454  1259lem1  16458  1259lem2  16459  1259lem3  16460  1259lem4  16461  1259lem5  16462  1259prm  16463  2503lem2  16465  2503prm  16467  4001lem1  16468  4001lem2  16469  4001lem4  16471  4001prm  16472  mcubic  25419  log2ublem3  25520  log2ub  25521  birthday  25526  chtub  25782  2lgsoddprmlem3c  25982  istrkg3ld  26241  usgr2wlkspthlem2  27533  elwwlks2ons3im  27727  umgrwwlks2on  27730  elwwlks2  27739  elwspths2spth  27740  clwwlknonex2lem1  27880  clwwlknonex2lem2  27881  3wlkdlem5  27936  3wlkdlem10  27942  upgr3v3e3cycl  27953  upgr4cycl4dv4e  27958  konigsberglem1  28025  konigsberglem2  28026  konigsberglem3  28027  numclwlk1  28144  frgrregord013  28168  ex-hash  28226  threehalves  30586  lmat22det  31082  fib3  31656  prodfzo03  31869  hgt750lemd  31914  hgt750lem  31917  hgt750lem2  31918  3cubeslem3l  39276  3cubeslem3r  39277  jm2.23  39586  lt3addmuld  41561  wallispilem4  42347  wallispi2lem1  42350  stirlinglem11  42363  fmtno0  43696  fmtno5lem4  43712  fmtno4prmfac  43728  fmtno4nprmfac193  43730  139prmALT  43753  31prm  43754  m7prm  43758  lighneallem4a  43767  41prothprmlem2  43777  2exp340mod341  43892  sbgoldbalt  43940  bgoldbtbndlem1  43964  tgoldbachlt  43975  pgrpgt2nabl  44408