Theorem 2p1e3 12435

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

Syntax hints:   = wceq 1537  (class class class)co 7448  1c1 11185   + caddc 11187  2c2 12348  3c3 12349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-3 12357

This theorem is referenced by:  1p2e3  12436  1p2e3ALT  12437  cnm2m1cnm3  12546  6t5e30  12865  7t5e35  12870  8t4e32  12875  9t4e36  12882  decbin3  12900  halfthird  12901  fz0to3un2pr  13686  fz0to4untppr  13687  fz0to5un2tp  13688  fzo0to42pr  13803  m1modge3gt1  13969  fac3  14329  hash3  14455  hashtplei  14533  hashtpg  14534  hash3tpexb  14543  s3len  14943  repsw3  15000  bpoly3  16106  bpoly4  16107  nn0o1gt2  16429  flodddiv4  16461  ge2nprmge4  16748  3exp3  17139  13prm  17163  37prm  17168  43prm  17169  83prm  17170  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem2  17185  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem4  17191  4001prm  17192  mcubic  26908  log2ublem3  27009  log2ub  27010  birthday  27015  chtub  27274  2lgsoddprmlem3c  27474  istrkg3ld  28487  usgr2wlkspthlem2  29794  elwwlks2ons3im  29987  umgrwwlks2on  29990  elwwlks2  29999  elwspths2spth  30000  clwwlknonex2lem1  30139  clwwlknonex2lem2  30140  3wlkdlem5  30195  3wlkdlem10  30201  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  numclwlk1  30403  frgrregord013  30427  ex-hash  30485  threehalves  32879  evl1deg2  33567  ply1dg3rt0irred  33572  lmat22det  33768  fib3  34368  prodfzo03  34580  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  aks4d1p1p2  42027  aks4d1p1p7  42031  aks4d1p1  42033  2np3bcnp1  42101  aks6d1c7lem1  42137  3cubeslem3l  42642  3cubeslem3r  42643  jm2.23  42953  resqrtvalex  43607  lt3addmuld  45216  wallispilem4  45989  wallispi2lem1  45992  stirlinglem11  46005  fmtno0  47414  fmtno5lem4  47430  fmtno4prmfac  47446  fmtno4nprmfac193  47448  139prmALT  47470  31prm  47471  m7prm  47474  lighneallem4a  47482  41prothprmlem2  47492  2exp340mod341  47607  sbgoldbalt  47655  bgoldbtbndlem1  47679  tgoldbachlt  47690  pgrpgt2nabl  48091  ackval2  48416  ackval3  48417  ackval0012  48423  ackval3012  48426