Definition df-3 12276

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 12268	. 2 class 3
2		c2 12267	. . 3 class 2
3		c1 11111	. . 3 class 1
4		caddc 11113	. . 3 class +
5	2, 3, 4	co 7409	. 2 class (2 + 1)
6	1, 5	wceq 1542	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12291  3re  12292  3cn  12293  3pos  12317  3m1e2  12340  2p2e4  12347  2p1e3  12354  3p3e6  12364  4p3e7  12366  5p3e8  12369  6p3e9  12372  3t3e9  12379  2lt3  12384  7p3e10  12752  7p6e13  12755  8p3e11  12758  8p5e13  12760  9p3e12  12765  9p4e13  12766  4t3e12  12775  5t3e15  12778  6t3e18  12782  7t3e21  12787  8t3e24  12793  9t3e27  12800  nn01to3  12925  fztpval  13563  fz0to3un2pr  13603  fz0to4untppr  13604  fzo0to42pr  13719  fzo1to4tp  13720  cu2  14164  i3  14167  binom3  14187  fac3  14240  hashtpg  14446  01sqrexlem7  15195  bpoly2  16001  bpoly4  16003  fsumcube  16004  ege2le3  16033  ef4p  16056  cos1bnd  16130  oddprmge3  16637  prmgaplem3  16986  13prm  17049  23prm  17052  43prm  17055  83prm  17056  163prm  17058  lt6abl  19763  cphipval  24760  vitalilem4  25128  itgcnlem  25307  dveflem  25496  sincosq3sgn  26010  sincosq4sgn  26011  tangtx  26015  sincos6thpi  26025  ang180lem2  26315  mcubic  26352  cubic2  26353  binom4  26355  dquartlem2  26357  quart1  26361  quartlem1  26362  log2ublem3  26453  basellem5  26589  basellem8  26592  basellem9  26593  ppi3  26675  cht3  26677  ppiublem1  26705  ppiublem2  26706  ppiub  26707  chtub  26715  bclbnd  26783  bposlem2  26788  bposlem9  26795  lgsdir2lem3  26830  dchrvmasumiflem1  27004  mulog2sumlem2  27038  pntlemk  27109  pntlemo  27110  axlowdimlem3  28202  axlowdimlem13  28212  axlowdimlem16  28215  axlowdimlem17  28216  2wlkdlem1  29179  elwwlks2s3  29205  elwspths2spth  29221  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  konigsberglem5  29509  ipval2  29960  stm1add3i  31500  stadd3i  31501  problem2  34651  problem4  34653  sinccvglem  34657  mblfinlem3  36527  heiborlem6  36684  aks4d1p1  40941  2ap1caineq  40961  fac2xp3  41020  nicomachus  41210  sn-0ne2  41279  3cubeslem2  41423  3cubeslem3r  41425  rmydioph  41753  rmxdioph  41755  expdiophlem2  41761  expdioph  41762  amgm3d  42951  stoweidlem26  44742  31prm  46265  lighneallem4b  46277  3odd  46376  sbgoldbo  46455  itcoval3  47351  ackval3  47369