Theorem 2p1e3 11767

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

Syntax hints:   = wceq 1538  (class class class)co 7135  1c1 10527   + caddc 10529  2c2 11680  3c3 11681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-3 11689

This theorem is referenced by:  1p2e3  11768  1p2e3ALT  11769  cnm2m1cnm3  11878  6t5e30  12193  7t5e35  12198  8t4e32  12203  9t4e36  12210  decbin3  12228  halfthird  12229  fz0to3un2pr  13004  fzo0to42pr  13119  m1modge3gt1  13281  fac3  13636  hash3  13763  hashtplei  13838  hashtpg  13839  s3len  14247  repsw3  14304  bpoly3  15404  bpoly4  15405  nn0o1gt2  15722  flodddiv4  15754  ge2nprmge4  16035  3exp3  16417  13prm  16441  37prm  16446  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem2  16463  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem4  16469  4001prm  16470  mcubic  25433  log2ublem3  25534  log2ub  25535  birthday  25540  chtub  25796  2lgsoddprmlem3c  25996  istrkg3ld  26255  usgr2wlkspthlem2  27547  elwwlks2ons3im  27740  umgrwwlks2on  27743  elwwlks2  27752  elwspths2spth  27753  clwwlknonex2lem1  27892  clwwlknonex2lem2  27893  3wlkdlem5  27948  3wlkdlem10  27954  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039  numclwlk1  28156  frgrregord013  28180  ex-hash  28238  threehalves  30617  lmat22det  31175  fib3  31771  prodfzo03  31984  hgt750lemd  32029  hgt750lem  32032  hgt750lem2  32033  2np3bcnp1  39348  3cubeslem3l  39627  3cubeslem3r  39628  jm2.23  39937  resqrtvalex  40345  lt3addmuld  41933  wallispilem4  42710  wallispi2lem1  42713  stirlinglem11  42726  fmtno0  44057  fmtno5lem4  44073  fmtno4prmfac  44089  fmtno4nprmfac193  44091  139prmALT  44113  31prm  44114  m7prm  44117  lighneallem4a  44126  41prothprmlem2  44136  2exp340mod341  44251  sbgoldbalt  44299  bgoldbtbndlem1  44323  tgoldbachlt  44334  pgrpgt2nabl  44768  ackval2  45096  ackval3  45097  ackval0012  45103  ackval3012  45106