Theorem 2p1e3 12408

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

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  2c2 12321  3c3 12322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-3 12330

This theorem is referenced by:  1p2e3  12409  1p2e3ALT  12410  cnm2m1cnm3  12519  6t5e30  12840  7t5e35  12845  8t4e32  12850  9t4e36  12857  decbin3  12875  halfthird  12876  fz0to3un2pr  13669  fz0to4untppr  13670  fz0to5un2tp  13671  fzo0to42pr  13792  m1modge3gt1  13959  fac3  14319  hash3  14445  hashtplei  14523  hashtpg  14524  hash3tpexb  14533  s3len  14933  repsw3  14990  bpoly3  16094  bpoly4  16095  nn0o1gt2  16418  flodddiv4  16452  ge2nprmge4  16738  3exp3  17129  13prm  17153  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem2  17175  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem4  17181  4001prm  17182  mcubic  26890  log2ublem3  26991  log2ub  26992  birthday  26997  chtub  27256  2lgsoddprmlem3c  27456  istrkg3ld  28469  usgr2wlkspthlem2  29778  elwwlks2ons3im  29974  umgrwwlks2on  29977  elwwlks2  29986  elwspths2spth  29987  clwwlknonex2lem1  30126  clwwlknonex2lem2  30127  3wlkdlem5  30182  3wlkdlem10  30188  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  numclwlk1  30390  frgrregord013  30414  ex-hash  30472  threehalves  32897  evl1deg2  33602  ply1dg3rt0irred  33607  lmat22det  33821  fib3  34405  prodfzo03  34618  hgt750lemd  34663  hgt750lem  34666  hgt750lem2  34667  aks4d1p1p2  42071  aks4d1p1p7  42075  aks4d1p1  42077  2np3bcnp1  42145  aks6d1c7lem1  42181  3cubeslem3l  42697  3cubeslem3r  42698  jm2.23  43008  resqrtvalex  43658  lt3addmuld  45313  wallispilem4  46083  wallispi2lem1  46086  stirlinglem11  46099  m1modnep2mod  47354  minusmodnep2tmod  47355  fmtno0  47527  fmtno5lem4  47543  fmtno4prmfac  47559  fmtno4nprmfac193  47561  139prmALT  47583  31prm  47584  m7prm  47587  lighneallem4a  47595  41prothprmlem2  47605  2exp340mod341  47720  sbgoldbalt  47768  bgoldbtbndlem1  47792  tgoldbachlt  47803  cycl3grtrilem  47913  gpg5order  48014  gpg3kgrtriexlem2  48040  gpg5gricstgr3  48046  pgrpgt2nabl  48282  ackval2  48603  ackval3  48604  ackval0012  48610  ackval3012  48613