Theorem 2p1e3 12370

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

Syntax hints:   = wceq 1534  (class class class)co 7414  1c1 11125   + caddc 11127  2c2 12283  3c3 12284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719  df-3 12292

This theorem is referenced by:  1p2e3  12371  1p2e3ALT  12372  cnm2m1cnm3  12481  6t5e30  12800  7t5e35  12805  8t4e32  12810  9t4e36  12817  decbin3  12835  halfthird  12836  fz0to3un2pr  13621  fzo0to42pr  13737  m1modge3gt1  13901  fac3  14257  hash3  14383  hashtplei  14463  hashtpg  14464  s3len  14863  repsw3  14920  bpoly3  16020  bpoly4  16021  nn0o1gt2  16343  flodddiv4  16375  ge2nprmge4  16657  3exp3  17046  13prm  17070  37prm  17075  43prm  17076  83prm  17077  139prm  17078  163prm  17079  317prm  17080  631prm  17081  1259lem1  17085  1259lem2  17086  1259lem3  17087  1259lem4  17088  1259lem5  17089  1259prm  17090  2503lem2  17092  2503prm  17094  4001lem1  17095  4001lem2  17096  4001lem4  17098  4001prm  17099  mcubic  26753  log2ublem3  26854  log2ub  26855  birthday  26860  chtub  27119  2lgsoddprmlem3c  27319  istrkg3ld  28239  usgr2wlkspthlem2  29546  elwwlks2ons3im  29739  umgrwwlks2on  29742  elwwlks2  29751  elwspths2spth  29752  clwwlknonex2lem1  29891  clwwlknonex2lem2  29892  3wlkdlem5  29947  3wlkdlem10  29953  upgr3v3e3cycl  29964  upgr4cycl4dv4e  29969  konigsberglem1  30036  konigsberglem2  30037  konigsberglem3  30038  numclwlk1  30155  frgrregord013  30179  ex-hash  30237  threehalves  32607  lmat22det  33346  fib3  33946  prodfzo03  34158  hgt750lemd  34203  hgt750lem  34206  hgt750lem2  34207  aks4d1p1p2  41465  aks4d1p1p7  41469  aks4d1p1  41471  2np3bcnp1  41535  3cubeslem3l  42018  3cubeslem3r  42019  jm2.23  42329  resqrtvalex  42988  lt3addmuld  44596  wallispilem4  45369  wallispi2lem1  45372  stirlinglem11  45385  fmtno0  46793  fmtno5lem4  46809  fmtno4prmfac  46825  fmtno4nprmfac193  46827  139prmALT  46849  31prm  46850  m7prm  46853  lighneallem4a  46861  41prothprmlem2  46871  2exp340mod341  46986  sbgoldbalt  47034  bgoldbtbndlem1  47058  tgoldbachlt  47069  pgrpgt2nabl  47343  ackval2  47668  ackval3  47669  ackval0012  47675  ackval3012  47678