Theorem 2p1e3 12377

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

Syntax hints:   = wceq 1570  (class class class)co 7410  1c1 11096   + caddc 11098  2c2 12290  3c3 12291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-3 12299

This theorem is referenced by:  1p2e3  12378  1p2e3ALT  12379  halfthird  12460  halfpm6th  12461  cnm2m1cnm3  12492  6t5e30  12818  7t5e35  12823  8t4e32  12828  9t4e36  12835  decbin3  12855  fz0to3un2pr  13653  fz0to4untppr  13654  fz0to5un2tp  13655  fzo0to42pr  13778  m1modge3gt1  13950  fac3  14312  hash3  14438  hashtplei  14517  hashtpg  14518  hash3tpexb  14527  s3len  14927  repsw3  14984  bpoly3  16107  bpoly4  16108  nn0o1gt2  16434  flodddiv4  16468  ge2nprmge4  16755  3exp3  17146  13prm  17171  37prm  17176  43prm  17177  83prm  17178  139prm  17179  163prm  17180  317prm  17181  631prm  17182  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  1259prm  17191  2503lem2  17193  2503prm  17195  4001lem1  17196  4001lem2  17197  4001lem4  17199  4001prm  17200  mcubic  27012  log2ublem3  27113  log2ub  27114  birthday  27119  chtub  27376  2lgsoddprmlem3c  27576  istrkg3ld  28730  usgr2wlkspthlem2  30107  elwwlks2ons3im  30303  usgrwwlks2on  30307  umgrwwlks2on  30308  elwwlks2  30318  elwspths2spth  30319  clwwlknonex2lem1  30458  clwwlknonex2lem2  30459  3wlkdlem5  30514  3wlkdlem10  30520  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  konigsberglem1  30603  konigsberglem2  30604  konigsberglem3  30605  numclwlk1  30722  frgrregord013  30746  ex-hash  30804  threehalves  33234  evl1deg2  33867  ply1dg3rt0irred  33874  cos9thpiminplylem1  34172  cos9thpiminplylem2  34173  cos9thpiminplylem5  34176  lmat22det  34212  fib3  34793  prodfzo03  34990  hgt750lemd  35035  hgt750lem  35038  hgt750lem2  35039  aks4d1p1p2  42837  aks4d1p1p7  42841  aks4d1p1  42843  2np3bcnp1  42911  aks6d1c7lem1  42947  3cubeslem3l  43417  3cubeslem3r  43418  jm2.23  43723  resqrtvalex  44371  lt3addmuld  46020  wallispilem4  46782  wallispi2lem1  46785  stirlinglem11  46798  sin3t  47608  sin5tlem4  47613  m1modnep2mod  48095  minusmodnep2tmod  48096  modm1nep2  48111  2timesltsqm1  48116  fmtno0  48292  fmtno5lem4  48308  fmtno4prmfac  48324  fmtno4nprmfac193  48326  139prmALT  48348  31prm  48349  m7prm  48352  lighneallem4a  48360  41prothprmlem2  48370  ppivalnnnprm  48380  2exp340mod341  48498  sbgoldbalt  48546  bgoldbtbndlem1  48570  tgoldbachlt  48581  cycl3grtrilem  48711  gpg5order  48825  gpg3kgrtriexlem2  48849  gpg5gricstgr3  48855  gpgprismgr4cycllem10  48869  pgnbgreunbgrlem2lem2  48880  pgrpgt2nabl  49146  ackval2  49462  ackval3  49463  ackval0012  49469  ackval3012  49472