Theorem 2p1e3 11528

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

Syntax hints:   = wceq 1601  (class class class)co 6924  1c1 10275   + caddc 10277  2c2 11434  3c3 11435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-3 11443

This theorem is referenced by:  1p2e3  11529  1p2e3ALT  11530  cnm2m1cnm3  11639  6t5e30  11958  7t5e35  11963  8t4e32  11968  9t4e36  11975  decbin3  11993  halfthird  11994  fz0to3un2pr  12764  fzo0to42pr  12878  m1modge3gt1  13040  fac3  13389  hash3  13512  hashtplei  13584  hashtpg  13585  s3len  14049  repsw3  14106  bpoly3  15195  bpoly4  15196  nn0o1gt2  15515  flodddiv4  15547  3exp3  16201  13prm  16225  37prm  16230  43prm  16231  83prm  16232  139prm  16233  163prm  16234  317prm  16235  631prm  16236  1259lem1  16240  1259lem2  16241  1259lem3  16242  1259lem4  16243  1259lem5  16244  1259prm  16245  2503lem2  16247  2503prm  16249  4001lem1  16250  4001lem2  16251  4001lem4  16253  4001prm  16254  dcubic1lem  25025  dcubic2  25026  mcubic  25029  log2ublem3  25131  log2ub  25132  birthday  25137  chtub  25393  2lgsoddprmlem3c  25593  istrkg3ld  25816  usgr2wlkspthlem2  27114  elwwlks2ons3im  27338  umgrwwlks2on  27341  elwwlks2  27350  elwspths2spth  27351  clwwlknonex2lem1  27513  clwwlknonex2lem2  27514  3wlkdlem5  27570  3wlkdlem10  27576  upgr3v3e3cycl  27587  upgr4cycl4dv4e  27592  konigsberglem1  27662  konigsberglem2  27663  konigsberglem3  27664  numclwlk1  27803  frgrregord013  27831  ex-hash  27889  threehalves  30189  lmat22det  30490  fib3  31068  prodfzo03  31287  hgt750lemd  31332  hgt750lem  31335  hgt750lem2  31336  jm2.23  38532  lt3addmuld  40434  wallispilem4  41222  wallispi2lem1  41225  stirlinglem11  41238  fmtno0  42483  fmtno5lem4  42499  fmtno4prmfac  42515  fmtno4nprmfac193  42517  139prmALT  42542  31prm  42543  m7prm  42547  lighneallem4a  42556  41prothprmlem2  42566  sbgoldbalt  42704  bgoldbtbndlem1  42728  tgoldbachlt  42739  pgrpgt2nabl  43172