Definition df-3 12226

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 12218	. 2 class 3
2		c2 12217	. . 3 class 2
3		c1 11045	. . 3 class 1
4		caddc 11047	. . 3 class +
5	2, 3, 4	co 7369	. 2 class (2 + 1)
6	1, 5	wceq 1540	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12241  3re  12242  3cn  12243  3pos  12267  3m1e2  12285  2p2e4  12292  2p1e3  12299  3p3e6  12309  4p3e7  12311  5p3e8  12314  6p3e9  12317  3t3e9  12324  2lt3  12329  7p3e10  12700  7p6e13  12703  8p3e11  12706  8p5e13  12708  9p3e12  12713  9p4e13  12714  4t3e12  12723  5t3e15  12726  6t3e18  12730  7t3e21  12735  8t3e24  12741  9t3e27  12748  nn01to3  12876  fztpval  13523  fz0to3un2pr  13566  fzo0to42pr  13690  fzo1to4tp  13691  cu2  14141  i3  14144  binom3  14165  fac3  14221  hashtpg  14426  01sqrexlem7  15190  bpoly2  15999  bpoly4  16001  fsumcube  16002  ege2le3  16032  ef4p  16057  cos1bnd  16131  oddprmge3  16646  prmgaplem3  17000  13prm  17062  23prm  17065  43prm  17068  83prm  17069  163prm  17071  lt6abl  19801  cphipval  25119  vitalilem4  25488  itgcnlem  25667  dveflem  25859  sincosq3sgn  26385  sincosq4sgn  26386  tangtx  26390  sincos6thpi  26401  ang180lem2  26696  mcubic  26733  cubic2  26734  binom4  26736  dquartlem2  26738  quart1  26742  quartlem1  26743  log2ublem3  26834  basellem5  26971  basellem8  26974  basellem9  26975  ppi3  27057  cht3  27059  ppiublem1  27089  ppiublem2  27090  ppiub  27091  chtub  27099  bclbnd  27167  bposlem2  27172  bposlem9  27179  lgsdir2lem3  27214  dchrvmasumiflem1  27388  mulog2sumlem2  27422  pntlemk  27493  pntlemo  27494  axlowdimlem3  28847  axlowdimlem13  28857  axlowdimlem16  28860  axlowdimlem17  28861  2wlkdlem1  29828  elwwlks2s3  29854  elwspths2spth  29870  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  konigsberglem5  30158  ipval2  30609  stm1add3i  32149  stadd3i  32150  problem2  35626  problem4  35628  sinccvglem  35632  mblfinlem3  37626  heiborlem6  37783  aks4d1p1  42037  2ap1caineq  42106  1p3e4  42220  nicomachus  42273  sn-0ne2  42367  3cubeslem2  42646  3cubeslem3r  42648  rmydioph  42976  rmxdioph  42978  expdiophlem2  42984  expdioph  42985  amgm3d  44161  stoweidlem26  45997  31prm  47571  lighneallem4b  47583  3odd  47682  sbgoldbo  47761  itcoval3  48627  ackval3  48645