Theorem 2p1e3 12354

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

Syntax hints:   = wceq 1542  (class class class)co 7409  1c1 11111   + caddc 11113  2c2 12267  3c3 12268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-3 12276

This theorem is referenced by:  1p2e3  12355  1p2e3ALT  12356  cnm2m1cnm3  12465  6t5e30  12784  7t5e35  12789  8t4e32  12794  9t4e36  12801  decbin3  12819  halfthird  12820  fz0to3un2pr  13603  fzo0to42pr  13719  m1modge3gt1  13883  fac3  14240  hash3  14366  hashtplei  14445  hashtpg  14446  s3len  14845  repsw3  14902  bpoly3  16002  bpoly4  16003  nn0o1gt2  16324  flodddiv4  16356  ge2nprmge4  16638  3exp3  17025  13prm  17049  37prm  17054  43prm  17055  83prm  17056  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem2  17071  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem4  17077  4001prm  17078  mcubic  26352  log2ublem3  26453  log2ub  26454  birthday  26459  chtub  26715  2lgsoddprmlem3c  26915  istrkg3ld  27712  usgr2wlkspthlem2  29015  elwwlks2ons3im  29208  umgrwwlks2on  29211  elwwlks2  29220  elwspths2spth  29221  clwwlknonex2lem1  29360  clwwlknonex2lem2  29361  3wlkdlem5  29416  3wlkdlem10  29422  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  konigsberglem1  29505  konigsberglem2  29506  konigsberglem3  29507  numclwlk1  29624  frgrregord013  29648  ex-hash  29706  threehalves  32081  lmat22det  32802  fib3  33402  prodfzo03  33615  hgt750lemd  33660  hgt750lem  33663  hgt750lem2  33664  aks4d1p1p2  40935  aks4d1p1p7  40939  aks4d1p1  40941  2np3bcnp1  40960  3cubeslem3l  41424  3cubeslem3r  41425  jm2.23  41735  resqrtvalex  42396  lt3addmuld  44011  wallispilem4  44784  wallispi2lem1  44787  stirlinglem11  44800  fmtno0  46208  fmtno5lem4  46224  fmtno4prmfac  46240  fmtno4nprmfac193  46242  139prmALT  46264  31prm  46265  m7prm  46268  lighneallem4a  46276  41prothprmlem2  46286  2exp340mod341  46401  sbgoldbalt  46449  bgoldbtbndlem1  46473  tgoldbachlt  46484  pgrpgt2nabl  47042  ackval2  47368  ackval3  47369  ackval0012  47375  ackval3012  47378