Theorem 2p1e3 12280

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

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   + caddc 11027  2c2 12198  3c3 12199

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 2706

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

This theorem is referenced by:  1p2e3  12281  1p2e3ALT  12282  halfthird  12360  halfpm6th  12361  cnm2m1cnm3  12392  6t5e30  12712  7t5e35  12717  8t4e32  12722  9t4e36  12729  decbin3  12747  fz0to3un2pr  13543  fz0to4untppr  13544  fz0to5un2tp  13545  fzo0to42pr  13667  m1modge3gt1  13839  fac3  14201  hash3  14327  hashtplei  14405  hashtpg  14406  hash3tpexb  14415  s3len  14815  repsw3  14872  bpoly3  15979  bpoly4  15980  nn0o1gt2  16306  flodddiv4  16340  ge2nprmge4  16626  3exp3  17017  13prm  17041  37prm  17046  43prm  17047  83prm  17048  139prm  17049  163prm  17050  317prm  17051  631prm  17052  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  1259prm  17061  2503lem2  17063  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem4  17069  4001prm  17070  mcubic  26811  log2ublem3  26912  log2ub  26913  birthday  26918  chtub  27177  2lgsoddprmlem3c  27377  istrkg3ld  28482  usgr2wlkspthlem2  29780  elwwlks2ons3im  29976  usgrwwlks2on  29980  umgrwwlks2on  29981  elwwlks2  29991  elwspths2spth  29992  clwwlknonex2lem1  30131  clwwlknonex2lem2  30132  3wlkdlem5  30187  3wlkdlem10  30193  upgr3v3e3cycl  30204  upgr4cycl4dv4e  30209  konigsberglem1  30276  konigsberglem2  30277  konigsberglem3  30278  numclwlk1  30395  frgrregord013  30419  ex-hash  30477  threehalves  32945  evl1deg2  33607  ply1dg3rt0irred  33614  cos9thpiminplylem1  33888  cos9thpiminplylem2  33889  cos9thpiminplylem5  33892  lmat22det  33928  fib3  34509  prodfzo03  34709  hgt750lemd  34754  hgt750lem  34757  hgt750lem2  34758  aks4d1p1p2  42263  aks4d1p1p7  42267  aks4d1p1  42269  2np3bcnp1  42337  aks6d1c7lem1  42373  3cubeslem3l  42870  3cubeslem3r  42871  jm2.23  43180  resqrtvalex  43828  lt3addmuld  45491  wallispilem4  46254  wallispi2lem1  46257  stirlinglem11  46270  m1modnep2mod  47540  minusmodnep2tmod  47541  modm1nep2  47556  fmtno0  47728  fmtno5lem4  47744  fmtno4prmfac  47760  fmtno4nprmfac193  47762  139prmALT  47784  31prm  47785  m7prm  47788  lighneallem4a  47796  41prothprmlem2  47806  2exp340mod341  47921  sbgoldbalt  47969  bgoldbtbndlem1  47993  tgoldbachlt  48004  cycl3grtrilem  48134  gpg5order  48248  gpg3kgrtriexlem2  48272  gpg5gricstgr3  48278  gpgprismgr4cycllem10  48292  pgnbgreunbgrlem2lem2  48303  pgrpgt2nabl  48554  ackval2  48870  ackval3  48871  ackval0012  48877  ackval3012  48880