Definition df-3 11702

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 11694	. 2 class 3
2		c2 11693	. . 3 class 2
3		c1 10538	. . 3 class 1
4		caddc 10540	. . 3 class +
5	2, 3, 4	co 7156	. 2 class (2 + 1)
6	1, 5	wceq 1537	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  11717  3re  11718  3cn  11719  3pos  11743  3m1e2  11766  2p2e4  11773  2p1e3  11780  3p3e6  11790  4p3e7  11792  5p3e8  11795  6p3e9  11798  3t3e9  11805  2lt3  11810  7p3e10  12174  7p6e13  12177  8p3e11  12180  8p5e13  12182  9p3e12  12187  9p4e13  12188  4t3e12  12197  5t3e15  12200  6t3e18  12204  7t3e21  12209  8t3e24  12215  9t3e27  12222  nn01to3  12342  fztpval  12970  fz0to3un2pr  13010  fz0to4untppr  13011  fzo0to42pr  13125  fzo1to4tp  13126  cu2  13564  i3  13567  binom3  13586  fac3  13641  hashtpg  13844  sqrlem7  14608  bpoly2  15411  bpoly4  15413  fsumcube  15414  ege2le3  15443  ef4p  15466  cos1bnd  15540  oddprmge3  16044  prmgaplem3  16389  13prm  16449  23prm  16452  43prm  16455  83prm  16456  163prm  16458  lt6abl  19015  cphipval  23846  vitalilem4  24212  itgcnlem  24390  dveflem  24576  sincosq3sgn  25086  sincosq4sgn  25087  tangtx  25091  sincos6thpi  25101  ang180lem2  25388  mcubic  25425  cubic2  25426  binom4  25428  dquartlem2  25430  quart1  25434  quartlem1  25435  log2ublem3  25526  basellem5  25662  basellem8  25665  basellem9  25666  ppi3  25748  cht3  25750  ppiublem1  25778  ppiublem2  25779  ppiub  25780  chtub  25788  bclbnd  25856  bposlem2  25861  bposlem9  25868  lgsdir2lem3  25903  dchrvmasumiflem1  26077  mulog2sumlem2  26111  pntlemk  26182  pntlemo  26183  axlowdimlem3  26730  axlowdimlem13  26740  axlowdimlem16  26743  axlowdimlem17  26744  2wlkdlem1  27704  elwwlks2s3  27730  elwspths2spth  27746  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  konigsberglem5  28035  ipval2  28484  stm1add3i  30024  stadd3i  30025  problem2  32909  problem4  32911  sinccvglem  32915  mblfinlem3  34946  heiborlem6  35109  fac2xp3  39143  sn-0ne2  39285  3cubeslem2  39331  3cubeslem3r  39333  rmydioph  39660  rmxdioph  39662  expdiophlem2  39668  expdioph  39669  amgm3d  40601  stoweidlem26  42360  31prm  43809  lighneallem4b  43823  3odd  43922  sbgoldbo  44001