Theorem 2p1e3 12477

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7418  1c1 11194   + caddc 11196  2c2 12390  3c3 12391

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 2733

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

This theorem is used by:  1p2e3  12478  1p2e3ALT  12479  halfthird  12560  halfpm6th  12561  cnm2m1cnm3  12592  6t5e30  12919  7t5e35  12924  8t4e32  12929  9t4e36  12936  decbin3  12956  fz0to3un2pr  13756  fz0to4untppr  13757  fz0to5un2tp  13758  fzo0to42pr  13881  m1modge3gt1  14054  fac3  14417  hash3  14543  hashtplei  14622  hashtpg  14623  hash3tpexb  14632  s3len  15038  repsw3  15097  bpoly3  16217  bpoly4  16218  nn0o1gt2  16544  flodddiv4  16578  ge2nprmge4  16870  3exp3  17262  13prm  17287  37prm  17292  43prm  17293  83prm  17294  139prm  17295  163prm  17296  317prm  17297  631prm  17298  1259lem1  17302  1259lem2  17303  1259lem3  17304  1259lem4  17305  1259lem5  17306  1259prm  17307  2503lem2  17309  2503prm  17311  4001lem1  17312  4001lem2  17313  4001lem4  17315  4001prm  17316  mcubic  27168  log2ublem3  27269  log2ub  27270  birthday  27275  chtub  27532  2lgsoddprmlem3c  27732  fltoprmgt3  27989  istrkg3ld  28916  usgr2wlkspthlem2  30337  elwwlks2ons3im  30536  usgrwwlks2on  30540  umgrwwlks2on  30541  elwwlks2  30551  elwspths2spth  30552  clwwlknonex2lem1  30691  clwwlknonex2lem2  30692  3wlkdlem5  30757  3wlkdlem10  30763  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  konigsberglem1  30846  konigsberglem2  30847  konigsberglem3  30848  numclwlk1  30965  frgrregord013  30989  ex-hash  31047  threehalves  33474  evl1deg2  34102  ply1dg3rt0irred  34109  cos9thpiminplylem1  34407  cos9thpiminplylem2  34408  cos9thpiminplylem5  34411  lmat22det  34447  fib3  35028  prodfzo03  35225  hgt750lemd  35270  hgt750lem  35273  hgt750lem2  35274  aks4d1p1p2  43100  aks4d1p1p7  43104  aks4d1p1  43106  2np3bcnp1  43174  aks6d1c7lem1  43210  2p3e5  43296  3cubeslem3l  43676  3cubeslem3r  43677  jm2.23  43982  resqrtvalex  44630  lt3addmuld  46286  wallispilem4  47047  wallispi2lem1  47050  stirlinglem11  47063  sin3t  47886  sin5tlem4  47891  m1modnep2mod  48397  minusmodnep2tmod  48398  modm1nep2  48413  2timesltsqm1  48418  fmtno0  48594  fmtno5lem4  48610  fmtno4prmfac  48626  fmtno4nprmfac193  48628  139prmALT  48650  31prm  48651  m7prm  48654  lighneallem4a  48662  41prothprmlem2  48672  ppivalnnnprm  48682  2exp340mod341  48800  sbgoldbalt  48848  bgoldbtbndlem1  48872  tgoldbachlt  48883  cycl3grtrilem  49013  gpg5order  49127  gpg3kgrtriexlem2  49151  gpg5gricstgr3  49157  gpgprismgr4cycllem10  49171  pgnbgreunbgrlem2lem2  49182  pgrpgt2nabl  49447  ackval2  49763  ackval3  49764  ackval0012  49770  ackval3012  49773  veronesevrowd  50948  veroquadgsumlem  50952