Theorem 2p1e3 12282

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

Syntax hints:   = wceq 1541  (class class class)co 7358  1c1 11027   + caddc 11029  2c2 12200  3c3 12201

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 2123  ax-ext 2708

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

This theorem is referenced by:  1p2e3  12283  1p2e3ALT  12284  halfthird  12362  halfpm6th  12363  cnm2m1cnm3  12394  6t5e30  12714  7t5e35  12719  8t4e32  12724  9t4e36  12731  decbin3  12749  fz0to3un2pr  13545  fz0to4untppr  13546  fz0to5un2tp  13547  fzo0to42pr  13669  m1modge3gt1  13841  fac3  14203  hash3  14329  hashtplei  14407  hashtpg  14408  hash3tpexb  14417  s3len  14817  repsw3  14874  bpoly3  15981  bpoly4  15982  nn0o1gt2  16308  flodddiv4  16342  ge2nprmge4  16628  3exp3  17019  13prm  17043  37prm  17048  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem2  17065  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem4  17071  4001prm  17072  mcubic  26813  log2ublem3  26914  log2ub  26915  birthday  26920  chtub  27179  2lgsoddprmlem3c  27379  istrkg3ld  28533  usgr2wlkspthlem2  29831  elwwlks2ons3im  30027  usgrwwlks2on  30031  umgrwwlks2on  30032  elwwlks2  30042  elwspths2spth  30043  clwwlknonex2lem1  30182  clwwlknonex2lem2  30183  3wlkdlem5  30238  3wlkdlem10  30244  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  numclwlk1  30446  frgrregord013  30470  ex-hash  30528  threehalves  32996  evl1deg2  33658  ply1dg3rt0irred  33665  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminplylem5  33943  lmat22det  33979  fib3  34560  prodfzo03  34760  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  aks4d1p1p2  42324  aks4d1p1p7  42328  aks4d1p1  42330  2np3bcnp1  42398  aks6d1c7lem1  42434  3cubeslem3l  42928  3cubeslem3r  42929  jm2.23  43238  resqrtvalex  43886  lt3addmuld  45549  wallispilem4  46312  wallispi2lem1  46315  stirlinglem11  46328  m1modnep2mod  47598  minusmodnep2tmod  47599  modm1nep2  47614  fmtno0  47786  fmtno5lem4  47802  fmtno4prmfac  47818  fmtno4nprmfac193  47820  139prmALT  47842  31prm  47843  m7prm  47846  lighneallem4a  47854  41prothprmlem2  47864  2exp340mod341  47979  sbgoldbalt  48027  bgoldbtbndlem1  48051  tgoldbachlt  48062  cycl3grtrilem  48192  gpg5order  48306  gpg3kgrtriexlem2  48330  gpg5gricstgr3  48336  gpgprismgr4cycllem10  48350  pgnbgreunbgrlem2lem2  48361  pgrpgt2nabl  48612  ackval2  48928  ackval3  48929  ackval0012  48935  ackval3012  48938