Theorem 2p1e3 11782

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

Syntax hints:   = wceq 1537  (class class class)co 7158  1c1 10540   + caddc 10542  2c2 11695  3c3 11696

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-3 11704

This theorem is referenced by:  1p2e3  11783  1p2e3ALT  11784  cnm2m1cnm3  11893  6t5e30  12208  7t5e35  12213  8t4e32  12218  9t4e36  12225  decbin3  12243  halfthird  12244  fz0to3un2pr  13012  fzo0to42pr  13127  m1modge3gt1  13289  fac3  13643  hash3  13770  hashtplei  13845  hashtpg  13846  s3len  14258  repsw3  14315  bpoly3  15414  bpoly4  15415  nn0o1gt2  15734  flodddiv4  15766  ge2nprmge4  16047  3exp3  16427  13prm  16451  37prm  16456  43prm  16457  83prm  16458  139prm  16459  163prm  16460  317prm  16461  631prm  16462  1259lem1  16466  1259lem2  16467  1259lem3  16468  1259lem4  16469  1259lem5  16470  1259prm  16471  2503lem2  16473  2503prm  16475  4001lem1  16476  4001lem2  16477  4001lem4  16479  4001prm  16480  mcubic  25427  log2ublem3  25528  log2ub  25529  birthday  25534  chtub  25790  2lgsoddprmlem3c  25990  istrkg3ld  26249  usgr2wlkspthlem2  27541  elwwlks2ons3im  27735  umgrwwlks2on  27738  elwwlks2  27747  elwspths2spth  27748  clwwlknonex2lem1  27888  clwwlknonex2lem2  27889  3wlkdlem5  27944  3wlkdlem10  27950  upgr3v3e3cycl  27961  upgr4cycl4dv4e  27966  konigsberglem1  28033  konigsberglem2  28034  konigsberglem3  28035  numclwlk1  28152  frgrregord013  28176  ex-hash  28234  threehalves  30593  lmat22det  31089  fib3  31663  prodfzo03  31876  hgt750lemd  31921  hgt750lem  31924  hgt750lem2  31925  3cubeslem3l  39290  3cubeslem3r  39291  jm2.23  39600  lt3addmuld  41575  wallispilem4  42360  wallispi2lem1  42363  stirlinglem11  42376  fmtno0  43709  fmtno5lem4  43725  fmtno4prmfac  43741  fmtno4nprmfac193  43743  139prmALT  43766  31prm  43767  m7prm  43771  lighneallem4a  43780  41prothprmlem2  43790  2exp340mod341  43905  sbgoldbalt  43953  bgoldbtbndlem1  43977  tgoldbachlt  43988  pgrpgt2nabl  44421