Theorem 2p1e3 12406

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7413  1c1 11125   + caddc 11127  2c2 12319  3c3 12320

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-3 12328

This theorem is used by:  1p2e3  12407  1p2e3ALT  12408  halfthird  12489  halfpm6th  12490  cnm2m1cnm3  12521  6t5e30  12848  7t5e35  12853  8t4e32  12858  9t4e36  12865  decbin3  12885  fz0to3un2pr  13684  fz0to4untppr  13685  fz0to5un2tp  13686  fzo0to42pr  13809  m1modge3gt1  13982  fac3  14344  hash3  14470  hashtplei  14549  hashtpg  14550  hash3tpexb  14559  s3len  14965  repsw3  15024  bpoly3  16144  bpoly4  16145  nn0o1gt2  16471  flodddiv4  16505  ge2nprmge4  16792  3exp3  17183  13prm  17208  37prm  17213  43prm  17214  83prm  17215  139prm  17216  163prm  17217  317prm  17218  631prm  17219  1259lem1  17223  1259lem2  17224  1259lem3  17225  1259lem4  17226  1259lem5  17227  1259prm  17228  2503lem2  17230  2503prm  17232  4001lem1  17233  4001lem2  17234  4001lem4  17236  4001prm  17237  mcubic  27084  log2ublem3  27185  log2ub  27186  birthday  27191  chtub  27448  2lgsoddprmlem3c  27648  istrkg3ld  28802  usgr2wlkspthlem2  30223  elwwlks2ons3im  30422  usgrwwlks2on  30426  umgrwwlks2on  30427  elwwlks2  30437  elwspths2spth  30438  clwwlknonex2lem1  30577  clwwlknonex2lem2  30578  3wlkdlem5  30643  3wlkdlem10  30649  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  konigsberglem1  30732  konigsberglem2  30733  konigsberglem3  30734  numclwlk1  30851  frgrregord013  30875  ex-hash  30933  threehalves  33360  evl1deg2  33987  ply1dg3rt0irred  33994  cos9thpiminplylem1  34292  cos9thpiminplylem2  34293  cos9thpiminplylem5  34296  lmat22det  34332  fib3  34914  prodfzo03  35111  hgt750lemd  35156  hgt750lem  35159  hgt750lem2  35160  aks4d1p1p2  42936  aks4d1p1p7  42940  aks4d1p1  42942  2np3bcnp1  43010  aks6d1c7lem1  43046  2p3e5  43132  3cubeslem3l  43531  3cubeslem3r  43532  jm2.23  43837  resqrtvalex  44485  lt3addmuld  46134  wallispilem4  46896  wallispi2lem1  46899  stirlinglem11  46912  sin3t  47735  sin5tlem4  47740  m1modnep2mod  48246  minusmodnep2tmod  48247  modm1nep2  48262  2timesltsqm1  48267  fmtno0  48443  fmtno5lem4  48459  fmtno4prmfac  48475  fmtno4nprmfac193  48477  139prmALT  48499  31prm  48500  m7prm  48503  lighneallem4a  48511  41prothprmlem2  48521  ppivalnnnprm  48531  2exp340mod341  48649  sbgoldbalt  48697  bgoldbtbndlem1  48721  tgoldbachlt  48732  cycl3grtrilem  48862  gpg5order  48976  gpg3kgrtriexlem2  49000  gpg5gricstgr3  49006  gpgprismgr4cycllem10  49020  pgnbgreunbgrlem2lem2  49031  pgrpgt2nabl  49296  ackval2  49612  ackval3  49613  ackval0012  49619  ackval3012  49622  veronesevrowd  50812  veroquadgsumlem  50816