Theorem 2p1e3 12353

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

Syntax hints:   = wceq 1559  (class class class)co 7391  1c1 11068   + caddc 11070  2c2 12266  3c3 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-3 12275

This theorem is referenced by:  1p2e3  12354  1p2e3ALT  12355  halfthird  12436  halfpm6th  12437  cnm2m1cnm3  12468  6t5e30  12794  7t5e35  12799  8t4e32  12804  9t4e36  12811  decbin3  12831  fz0to3un2pr  13628  fz0to4untppr  13629  fz0to5un2tp  13630  fzo0to42pr  13753  m1modge3gt1  13925  fac3  14287  hash3  14413  hashtplei  14491  hashtpg  14492  hash3tpexb  14501  s3len  14901  repsw3  14958  bpoly3  16079  bpoly4  16080  nn0o1gt2  16406  flodddiv4  16440  ge2nprmge4  16727  3exp3  17118  13prm  17143  37prm  17148  43prm  17149  83prm  17150  139prm  17151  163prm  17152  317prm  17153  631prm  17154  1259lem1  17158  1259lem2  17159  1259lem3  17160  1259lem4  17161  1259lem5  17162  1259prm  17163  2503lem2  17165  2503prm  17167  4001lem1  17168  4001lem2  17169  4001lem4  17171  4001prm  17172  mcubic  26900  log2ublem3  27001  log2ub  27002  birthday  27007  chtub  27264  2lgsoddprmlem3c  27464  istrkg3ld  28618  usgr2wlkspthlem2  29915  elwwlks2ons3im  30111  usgrwwlks2on  30115  umgrwwlks2on  30116  elwwlks2  30126  elwspths2spth  30127  clwwlknonex2lem1  30266  clwwlknonex2lem2  30267  3wlkdlem5  30322  3wlkdlem10  30328  upgr3v3e3cycl  30339  upgr4cycl4dv4e  30344  konigsberglem1  30411  konigsberglem2  30412  konigsberglem3  30413  numclwlk1  30530  frgrregord013  30554  ex-hash  30612  threehalves  33053  evl1deg2  33734  ply1dg3rt0irred  33741  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  cos9thpiminplylem5  34044  lmat22det  34080  fib3  34661  prodfzo03  34858  hgt750lemd  34903  hgt750lem  34906  hgt750lem2  34907  aks4d1p1p2  42648  aks4d1p1p7  42652  aks4d1p1  42654  2np3bcnp1  42722  aks6d1c7lem1  42758  3cubeslem3l  43228  3cubeslem3r  43229  jm2.23  43534  resqrtvalex  44182  lt3addmuld  45841  wallispilem4  46603  wallispi2lem1  46606  stirlinglem11  46619  sin3t  47426  sin5tlem4  47431  m1modnep2mod  47913  minusmodnep2tmod  47914  modm1nep2  47929  2timesltsqm1  47934  fmtno0  48110  fmtno5lem4  48126  fmtno4prmfac  48142  fmtno4nprmfac193  48144  139prmALT  48166  31prm  48167  m7prm  48170  lighneallem4a  48178  41prothprmlem2  48188  ppivalnnnprm  48198  2exp340mod341  48316  sbgoldbalt  48364  bgoldbtbndlem1  48388  tgoldbachlt  48399  cycl3grtrilem  48529  gpg5order  48643  gpg3kgrtriexlem2  48667  gpg5gricstgr3  48673  gpgprismgr4cycllem10  48687  pgnbgreunbgrlem2lem2  48698  pgrpgt2nabl  48949  ackval2  49265  ackval3  49266  ackval0012  49272  ackval3012  49275