Definition df-3 12331

Description: Define the number 3. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-3	⊢ 3 = (2 + 1)

Detailed syntax breakdown of Definition df-3

Step	Hyp	Ref	Expression
1		c3 12323	. 2 class 3
2		c2 12322	. . 3 class 2
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7416	. 2 class (2 + 1)
6	1, 5	wceq 1570	1 wff 3 = (2 + 1)

This definition is used by:  3nn  12347  3re  12348  3cn  12349  3m1e2  12395  2p2e4  12402  2p1e3  12409  3p3e6  12419  4p3e7  12421  5p3e8  12424  6p3e9  12427  3t3e9  12435  2lt3  12441  7p3e10  12819  7p6e13  12822  8p3e11  12825  8p5e13  12827  9p3e12  12832  9p4e13  12833  4t3e12  12842  5t3e15  12845  6t3e18  12849  7t3e21  12854  8t3e24  12860  9t3e27  12867  nn01to3  12993  fztpval  13643  fz0to3un2pr  13686  fzo0to42pr  13811  fzo1to4tp  13812  cu2  14266  i3  14269  binom3  14290  fac3  14346  hashtpg  14552  01sqrexlem7  15337  bpoly2  16147  bpoly4  16149  fsumcube  16150  ege2le3  16180  ef4p  16205  cos1bnd  16279  oddprmge3  16795  prmgaplem3  17149  13prm  17212  23prm  17215  43prm  17218  83prm  17219  163prm  17221  lt6abl  20023  cphipval  25472  vitalilem4  25840  itgcnlem  26019  dveflem  26208  sincosq3sgn  26735  sincosq4sgn  26736  tangtx  26740  sincos6thpi  26751  ang180lem2  27045  mcubic  27082  cubic2  27083  binom4  27085  dquartlem2  27087  quart1  27091  quartlem1  27092  log2ublem3  27183  basellem5  27319  basellem9  27323  ppi3  27405  cht3  27407  ppiublem1  27436  ppiublem2  27437  ppiub  27438  chtub  27446  bclbnd  27514  bposlem2  27519  bposlem9  27526  lgsdir2lem3  27561  dchrvmasumiflem1  27735  mulog2sumlem2  27769  pntlemk  27840  pntlemo  27841  axlowdimlem3  29387  axlowdimlem13  29397  axlowdimlem16  29400  axlowdimlem17  29401  2wlkdlem1  30379  elwwlks2s3  30405  elwspths2spth  30424  upgr3v3e3cycl  30646  upgr4cycl4dv4e  30651  konigsberglem5  30722  ipval2  31174  stm1add3i  32714  stadd3i  32715  problem2  36232  problem4  36234  sinccvglem  36238  mblfinlem3  38395  heiborlem6  38553  aks4d1p1  42929  2ap1caineq  42998  1p3e4  43113  nicomachus  43174  sn-0ne2  43268  3cubeslem2  43517  3cubeslem3r  43519  rmydioph  43842  rmxdioph  43844  expdiophlem2  43850  expdioph  43851  amgm3d  45026  stoweidlem26  46841  sin3t  47722  cos3t  47723  sin5tlem1  47724  goldpolyfactor  47732  2timesltsq  48253  2timesltsqm1  48254  31prm  48487  lighneallem4b  48499  nprmdvdsfacm1lem2  48511  3odd  48611  sbgoldbo  48690  itcoval3  49582  ackval3  49600