Definition df-3 12257

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 12249	. 2 class 3
2		c2 12248	. . 3 class 2
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7390	. 2 class (2 + 1)
6	1, 5	wceq 1540	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12272  3re  12273  3cn  12274  3pos  12298  3m1e2  12316  2p2e4  12323  2p1e3  12330  3p3e6  12340  4p3e7  12342  5p3e8  12345  6p3e9  12348  3t3e9  12355  2lt3  12360  7p3e10  12731  7p6e13  12734  8p3e11  12737  8p5e13  12739  9p3e12  12744  9p4e13  12745  4t3e12  12754  5t3e15  12757  6t3e18  12761  7t3e21  12766  8t3e24  12772  9t3e27  12779  nn01to3  12907  fztpval  13554  fz0to3un2pr  13597  fzo0to42pr  13721  fzo1to4tp  13722  cu2  14172  i3  14175  binom3  14196  fac3  14252  hashtpg  14457  01sqrexlem7  15221  bpoly2  16030  bpoly4  16032  fsumcube  16033  ege2le3  16063  ef4p  16088  cos1bnd  16162  oddprmge3  16677  prmgaplem3  17031  13prm  17093  23prm  17096  43prm  17099  83prm  17100  163prm  17102  lt6abl  19832  cphipval  25150  vitalilem4  25519  itgcnlem  25698  dveflem  25890  sincosq3sgn  26416  sincosq4sgn  26417  tangtx  26421  sincos6thpi  26432  ang180lem2  26727  mcubic  26764  cubic2  26765  binom4  26767  dquartlem2  26769  quart1  26773  quartlem1  26774  log2ublem3  26865  basellem5  27002  basellem8  27005  basellem9  27006  ppi3  27088  cht3  27090  ppiublem1  27120  ppiublem2  27121  ppiub  27122  chtub  27130  bclbnd  27198  bposlem2  27203  bposlem9  27210  lgsdir2lem3  27245  dchrvmasumiflem1  27419  mulog2sumlem2  27453  pntlemk  27524  pntlemo  27525  axlowdimlem3  28878  axlowdimlem13  28888  axlowdimlem16  28891  axlowdimlem17  28892  2wlkdlem1  29862  elwwlks2s3  29888  elwspths2spth  29904  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  konigsberglem5  30192  ipval2  30643  stm1add3i  32183  stadd3i  32184  problem2  35660  problem4  35662  sinccvglem  35666  mblfinlem3  37660  heiborlem6  37817  aks4d1p1  42071  2ap1caineq  42140  1p3e4  42254  nicomachus  42307  sn-0ne2  42401  3cubeslem2  42680  3cubeslem3r  42682  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  amgm3d  44195  stoweidlem26  46031  31prm  47602  lighneallem4b  47614  3odd  47713  sbgoldbo  47792  itcoval3  48658  ackval3  48676