Theorem 2p1e3 11343

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

Syntax hints:   = wceq 1632  (class class class)co 6813  1c1 10129   + caddc 10131  2c2 11262  3c3 11263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-3 11272

This theorem is referenced by:  1p2e3  11344  cnm2m1cnm3  11477  6t5e30  11836  6t5e30OLD  11837  7t5e35  11843  8t4e32  11848  9t4e36  11857  decbin3  11876  halfthird  11877  fz0to3un2pr  12635  m1modge3gt1  12911  fac3  13261  hash3  13386  hashtplei  13458  hashtpg  13459  s3len  13839  repsw3  13895  bpoly3  14988  bpoly4  14989  nn0o1gt2  15299  flodddiv4  15339  3exp3  16000  13prm  16025  37prm  16030  43prm  16031  83prm  16032  139prm  16033  163prm  16034  317prm  16035  631prm  16036  1259lem1  16040  1259lem2  16041  1259lem3  16042  1259lem4  16043  1259lem5  16044  1259prm  16045  2503lem2  16047  2503prm  16049  4001lem1  16050  4001lem2  16051  4001lem4  16053  4001prm  16054  dcubic1lem  24769  dcubic2  24770  mcubic  24773  log2ublem3  24874  log2ub  24875  birthday  24880  chtub  25136  2lgsoddprmlem3c  25336  istrkg3ld  25559  usgr2wlkspthlem2  26864  elwwlks2ons3im  27074  elwwlks2ons3OLD  27076  umgrwwlks2on  27078  elwwlks2  27088  elwspths2spth  27089  clwwlknonex2lem1  27256  clwwlknonex2lem2  27257  3wlkdlem5  27315  3wlkdlem10  27321  upgr3v3e3cycl  27332  upgr4cycl4dv4e  27337  konigsberglem1  27404  konigsberglem2  27405  konigsberglem3  27406  numclwlk1  27532  frgrregord013  27563  ex-hash  27621  threehalves  29932  lmat22det  30197  fib3  30774  prodfzo03  30990  hgt750lemd  31035  hgt750lem  31038  hgt750lem2  31039  jm2.23  38065  lt3addmuld  40014  wallispilem4  40788  wallispi2lem1  40791  stirlinglem11  40804  fmtno0  41962  fmtno5lem4  41978  fmtno4prmfac  41994  fmtno4nprmfac193  41996  139prmALT  42021  31prm  42022  m7prm  42026  lighneallem4a  42035  41prothprmlem2  42045  sbgoldbalt  42179  bgoldbtbndlem1  42203  tgoldbachlt  42214  tgoldbachltOLD  42220  pgrpgt2nabl  42657