Definition df-3 12250

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 12242	. 2 class 3
2		c2 12241	. . 3 class 2
3		c1 11069	. . 3 class 1
4		caddc 11071	. . 3 class +
5	2, 3, 4	co 7387	. 2 class (2 + 1)
6	1, 5	wceq 1540	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12265  3re  12266  3cn  12267  3pos  12291  3m1e2  12309  2p2e4  12316  2p1e3  12323  3p3e6  12333  4p3e7  12335  5p3e8  12338  6p3e9  12341  3t3e9  12348  2lt3  12353  7p3e10  12724  7p6e13  12727  8p3e11  12730  8p5e13  12732  9p3e12  12737  9p4e13  12738  4t3e12  12747  5t3e15  12750  6t3e18  12754  7t3e21  12759  8t3e24  12765  9t3e27  12772  nn01to3  12900  fztpval  13547  fz0to3un2pr  13590  fzo0to42pr  13714  fzo1to4tp  13715  cu2  14165  i3  14168  binom3  14189  fac3  14245  hashtpg  14450  01sqrexlem7  15214  bpoly2  16023  bpoly4  16025  fsumcube  16026  ege2le3  16056  ef4p  16081  cos1bnd  16155  oddprmge3  16670  prmgaplem3  17024  13prm  17086  23prm  17089  43prm  17092  83prm  17093  163prm  17095  lt6abl  19825  cphipval  25143  vitalilem4  25512  itgcnlem  25691  dveflem  25883  sincosq3sgn  26409  sincosq4sgn  26410  tangtx  26414  sincos6thpi  26425  ang180lem2  26720  mcubic  26757  cubic2  26758  binom4  26760  dquartlem2  26762  quart1  26766  quartlem1  26767  log2ublem3  26858  basellem5  26995  basellem8  26998  basellem9  26999  ppi3  27081  cht3  27083  ppiublem1  27113  ppiublem2  27114  ppiub  27115  chtub  27123  bclbnd  27191  bposlem2  27196  bposlem9  27203  lgsdir2lem3  27238  dchrvmasumiflem1  27412  mulog2sumlem2  27446  pntlemk  27517  pntlemo  27518  axlowdimlem3  28871  axlowdimlem13  28881  axlowdimlem16  28884  axlowdimlem17  28885  2wlkdlem1  29855  elwwlks2s3  29881  elwspths2spth  29897  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  konigsberglem5  30185  ipval2  30636  stm1add3i  32176  stadd3i  32177  problem2  35653  problem4  35655  sinccvglem  35659  mblfinlem3  37653  heiborlem6  37810  aks4d1p1  42064  2ap1caineq  42133  1p3e4  42247  nicomachus  42300  sn-0ne2  42394  3cubeslem2  42673  3cubeslem3r  42675  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  amgm3d  44188  stoweidlem26  46024  31prm  47598  lighneallem4b  47610  3odd  47709  sbgoldbo  47788  itcoval3  48654  ackval3  48672