Definition df-3 12283

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 12275	. 2 class 3
2		c2 12274	. . 3 class 2
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7398	. 2 class (2 + 1)
6	1, 5	wceq 1562	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12299  3re  12300  3cn  12301  3m1e2  12347  2p2e4  12354  2p1e3  12361  3p3e6  12371  4p3e7  12373  5p3e8  12376  6p3e9  12379  3t3e9  12387  2lt3  12393  7p3e10  12770  7p6e13  12773  8p3e11  12776  8p5e13  12778  9p3e12  12783  9p4e13  12784  4t3e12  12793  5t3e15  12796  6t3e18  12800  7t3e21  12805  8t3e24  12811  9t3e27  12818  nn01to3  12944  fztpval  13593  fz0to3un2pr  13636  fzo0to42pr  13761  fzo1to4tp  13762  cu2  14215  i3  14218  binom3  14239  fac3  14295  hashtpg  14500  01sqrexlem7  15277  bpoly2  16089  bpoly4  16091  fsumcube  16092  ege2le3  16122  ef4p  16147  cos1bnd  16221  oddprmge3  16737  prmgaplem3  17091  13prm  17154  23prm  17157  43prm  17160  83prm  17161  163prm  17163  lt6abl  19937  cphipval  25307  vitalilem4  25675  itgcnlem  25854  dveflem  26043  sincosq3sgn  26567  sincosq4sgn  26568  tangtx  26572  sincos6thpi  26583  ang180lem2  26877  mcubic  26914  cubic2  26915  binom4  26917  dquartlem2  26919  quart1  26923  quartlem1  26924  log2ublem3  27015  basellem5  27151  basellem8  27154  basellem9  27155  ppi3  27237  cht3  27239  ppiublem1  27268  ppiublem2  27269  ppiub  27270  chtub  27278  bclbnd  27346  bposlem2  27351  bposlem9  27358  lgsdir2lem3  27393  dchrvmasumiflem1  27567  mulog2sumlem2  27601  pntlemk  27672  pntlemo  27673  axlowdimlem3  29147  axlowdimlem13  29157  axlowdimlem16  29160  axlowdimlem17  29161  2wlkdlem1  30127  elwwlks2s3  30153  elwspths2spth  30172  upgr3v3e3cycl  30384  upgr4cycl4dv4e  30389  konigsberglem5  30460  ipval2  30912  stm1add3i  32452  stadd3i  32453  problem2  36021  problem4  36023  sinccvglem  36027  mblfinlem3  38163  heiborlem6  38320  aks4d1p1  42698  2ap1caineq  42767  1p3e4  42879  nicomachus  42926  sn-0ne2  43020  3cubeslem2  43271  3cubeslem3r  43273  rmydioph  43596  rmxdioph  43598  expdiophlem2  43604  expdioph  43605  amgm3d  44780  stoweidlem26  46605  sin3t  47470  cos3t  47471  sin5tlem1  47472  2timesltsq  47977  2timesltsqm1  47978  31prm  48211  lighneallem4b  48223  nprmdvdsfacm1lem2  48235  3odd  48335  sbgoldbo  48414  itcoval3  49292  ackval3  49310