Theorem 2p1e3 12323

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  2c2 12241  3c3 12242

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  1p2e3  12324  1p2e3ALT  12325  halfthird  12403  halfpm6th  12404  cnm2m1cnm3  12435  6t5e30  12756  7t5e35  12761  8t4e32  12766  9t4e36  12773  decbin3  12791  fz0to3un2pr  13590  fz0to4untppr  13591  fz0to5un2tp  13592  fzo0to42pr  13714  m1modge3gt1  13883  fac3  14245  hash3  14371  hashtplei  14449  hashtpg  14450  hash3tpexb  14459  s3len  14860  repsw3  14917  bpoly3  16024  bpoly4  16025  nn0o1gt2  16351  flodddiv4  16385  ge2nprmge4  16671  3exp3  17062  13prm  17086  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem2  17108  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem4  17114  4001prm  17115  mcubic  26757  log2ublem3  26858  log2ub  26859  birthday  26864  chtub  27123  2lgsoddprmlem3c  27323  istrkg3ld  28388  usgr2wlkspthlem2  29688  elwwlks2ons3im  29884  umgrwwlks2on  29887  elwwlks2  29896  elwspths2spth  29897  clwwlknonex2lem1  30036  clwwlknonex2lem2  30037  3wlkdlem5  30092  3wlkdlem10  30098  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  numclwlk1  30300  frgrregord013  30324  ex-hash  30382  threehalves  32835  evl1deg2  33546  ply1dg3rt0irred  33551  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem5  33776  lmat22det  33812  fib3  34394  prodfzo03  34594  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  aks4d1p1p2  42058  aks4d1p1p7  42062  aks4d1p1  42064  2np3bcnp1  42132  aks6d1c7lem1  42168  3cubeslem3l  42674  3cubeslem3r  42675  jm2.23  42985  resqrtvalex  43634  lt3addmuld  45299  wallispilem4  46066  wallispi2lem1  46069  stirlinglem11  46082  m1modnep2mod  47353  minusmodnep2tmod  47354  modm1nep2  47369  fmtno0  47541  fmtno5lem4  47557  fmtno4prmfac  47573  fmtno4nprmfac193  47575  139prmALT  47597  31prm  47598  m7prm  47601  lighneallem4a  47609  41prothprmlem2  47619  2exp340mod341  47734  sbgoldbalt  47782  bgoldbtbndlem1  47806  tgoldbachlt  47817  cycl3grtrilem  47945  gpg5order  48051  gpg3kgrtriexlem2  48075  gpg5gricstgr3  48081  gpgprismgr4cycllem10  48094  pgnbgreunbgrlem2lem2  48105  pgrpgt2nabl  48354  ackval2  48671  ackval3  48672  ackval0012  48678  ackval3012  48681