Theorem 2p1e3 11151

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 11080	. 2 |- 3 = ( 2 + 1 )
2	1	eqcomi 2631	1 |- ( 2 + 1 ) = 3

Syntax hints:   = wceq 1483  (class class class)co 6650   1c1 9937   + caddc 9939   2c2 11070   3c3 11071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-3 11080

This theorem is referenced by:  1p2e3  11152  cnm2m1cnm3  11285  6t5e30  11644  6t5e30OLD  11645  7t5e35  11651  8t4e32  11656  9t4e36  11665  decbin3  11684  halfthird  11685  fz0to3un2pr  12441  m1modge3gt1  12717  fac3  13067  hash3  13194  hashtplei  13266  hashtpg  13267  s3len  13639  repsw3  13694  bpoly3  14789  bpoly4  14790  nn0o1gt2  15097  flodddiv4  15137  3exp3  15798  13prm  15823  37prm  15828  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem2  15845  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem4  15851  4001prm  15852  dcubic1lem  24570  dcubic2  24571  mcubic  24574  log2ublem3  24675  log2ub  24676  birthday  24681  chtub  24937  2lgsoddprmlem3c  25137  istrkg3ld  25360  usgr2wlkspthlem2  26654  wwlks2onv  26847  elwwlks2ons3  26848  umgrwwlks2on  26850  elwwlks2  26861  elwspths2spth  26862  3wlkdlem5  27023  3wlkdlem10  27029  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  numclwwlkovf2exlem1  27211  numclwwlkovf2exlem2  27212  frgrregord013  27253  ex-hash  27310  threehalves  29623  lmat22det  29888  fib3  30465  prodfzo03  30681  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  jm2.23  37563  lt3addmuld  39515  wallispilem4  40285  wallispi2lem1  40288  stirlinglem11  40301  fmtno0  41452  fmtno5lem4  41468  fmtno4prmfac  41484  fmtno4nprmfac193  41486  139prmALT  41511  31prm  41512  m7prm  41516  lighneallem4a  41525  41prothprmlem2  41535  sbgoldbalt  41669  bgoldbtbndlem1  41693  tgoldbachlt  41704  tgoldbachltOLD  41710  pgrpgt2nabl  42147