Theorem 2p1e3 12257

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

Syntax hints:   = wceq 1541  (class class class)co 7341  1c1 11002   + caddc 11004  2c2 12175  3c3 12176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-3 12184

This theorem is referenced by:  1p2e3  12258  1p2e3ALT  12259  halfthird  12337  halfpm6th  12338  cnm2m1cnm3  12369  6t5e30  12690  7t5e35  12695  8t4e32  12700  9t4e36  12707  decbin3  12725  fz0to3un2pr  13524  fz0to4untppr  13525  fz0to5un2tp  13526  fzo0to42pr  13648  m1modge3gt1  13820  fac3  14182  hash3  14308  hashtplei  14386  hashtpg  14387  hash3tpexb  14396  s3len  14796  repsw3  14853  bpoly3  15960  bpoly4  15961  nn0o1gt2  16287  flodddiv4  16321  ge2nprmge4  16607  3exp3  16998  13prm  17022  37prm  17027  43prm  17028  83prm  17029  139prm  17030  163prm  17031  317prm  17032  631prm  17033  1259lem1  17037  1259lem2  17038  1259lem3  17039  1259lem4  17040  1259lem5  17041  1259prm  17042  2503lem2  17044  2503prm  17046  4001lem1  17047  4001lem2  17048  4001lem4  17050  4001prm  17051  mcubic  26779  log2ublem3  26880  log2ub  26881  birthday  26886  chtub  27145  2lgsoddprmlem3c  27345  istrkg3ld  28434  usgr2wlkspthlem2  29731  elwwlks2ons3im  29927  umgrwwlks2on  29930  elwwlks2  29939  elwspths2spth  29940  clwwlknonex2lem1  30079  clwwlknonex2lem2  30080  3wlkdlem5  30135  3wlkdlem10  30141  upgr3v3e3cycl  30152  upgr4cycl4dv4e  30157  konigsberglem1  30224  konigsberglem2  30225  konigsberglem3  30226  numclwlk1  30343  frgrregord013  30367  ex-hash  30425  threehalves  32887  evl1deg2  33532  ply1dg3rt0irred  33538  cos9thpiminplylem1  33787  cos9thpiminplylem2  33788  cos9thpiminplylem5  33791  lmat22det  33827  fib3  34408  prodfzo03  34608  hgt750lemd  34653  hgt750lem  34656  hgt750lem2  34657  aks4d1p1p2  42103  aks4d1p1p7  42107  aks4d1p1  42109  2np3bcnp1  42177  aks6d1c7lem1  42213  3cubeslem3l  42719  3cubeslem3r  42720  jm2.23  43029  resqrtvalex  43678  lt3addmuld  45342  wallispilem4  46106  wallispi2lem1  46109  stirlinglem11  46122  m1modnep2mod  47383  minusmodnep2tmod  47384  modm1nep2  47399  fmtno0  47571  fmtno5lem4  47587  fmtno4prmfac  47603  fmtno4nprmfac193  47605  139prmALT  47627  31prm  47628  m7prm  47631  lighneallem4a  47639  41prothprmlem2  47649  2exp340mod341  47764  sbgoldbalt  47812  bgoldbtbndlem1  47836  tgoldbachlt  47847  cycl3grtrilem  47977  gpg5order  48091  gpg3kgrtriexlem2  48115  gpg5gricstgr3  48121  gpgprismgr4cycllem10  48135  pgnbgreunbgrlem2lem2  48146  pgrpgt2nabl  48397  ackval2  48714  ackval3  48715  ackval0012  48721  ackval3012  48724