Definition df-3 12223

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 12215	. 2 class 3
2		c2 12214	. . 3 class 2
3		c1 11041	. . 3 class 1
4		caddc 11043	. . 3 class +
5	2, 3, 4	co 7370	. 2 class (2 + 1)
6	1, 5	wceq 1542	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12238  3re  12239  3cn  12240  3pos  12264  3m1e2  12282  2p2e4  12289  2p1e3  12296  3p3e6  12306  4p3e7  12308  5p3e8  12311  6p3e9  12314  3t3e9  12321  2lt3  12326  7p3e10  12696  7p6e13  12699  8p3e11  12702  8p5e13  12704  9p3e12  12709  9p4e13  12710  4t3e12  12719  5t3e15  12722  6t3e18  12726  7t3e21  12731  8t3e24  12737  9t3e27  12744  nn01to3  12868  fztpval  13516  fz0to3un2pr  13559  fzo0to42pr  13683  fzo1to4tp  13684  cu2  14137  i3  14140  binom3  14161  fac3  14217  hashtpg  14422  01sqrexlem7  15185  bpoly2  15994  bpoly4  15996  fsumcube  15997  ege2le3  16027  ef4p  16052  cos1bnd  16126  oddprmge3  16641  prmgaplem3  16995  13prm  17057  23prm  17060  43prm  17063  83prm  17064  163prm  17066  lt6abl  19841  cphipval  25216  vitalilem4  25585  itgcnlem  25764  dveflem  25956  sincosq3sgn  26482  sincosq4sgn  26483  tangtx  26487  sincos6thpi  26498  ang180lem2  26793  mcubic  26830  cubic2  26831  binom4  26833  dquartlem2  26835  quart1  26839  quartlem1  26840  log2ublem3  26931  basellem5  27068  basellem8  27071  basellem9  27072  ppi3  27154  cht3  27156  ppiublem1  27186  ppiublem2  27187  ppiub  27188  chtub  27196  bclbnd  27264  bposlem2  27269  bposlem9  27276  lgsdir2lem3  27311  dchrvmasumiflem1  27485  mulog2sumlem2  27519  pntlemk  27590  pntlemo  27591  axlowdimlem3  29035  axlowdimlem13  29045  axlowdimlem16  29048  axlowdimlem17  29049  2wlkdlem1  30016  elwwlks2s3  30042  elwspths2spth  30061  upgr3v3e3cycl  30273  upgr4cycl4dv4e  30278  konigsberglem5  30349  ipval2  30801  stm1add3i  32341  stadd3i  32342  problem2  35888  problem4  35890  sinccvglem  35894  mblfinlem3  37939  heiborlem6  38096  aks4d1p1  42475  2ap1caineq  42544  1p3e4  42658  nicomachus  42711  sn-0ne2  42805  3cubeslem2  43071  3cubeslem3r  43073  rmydioph  43400  rmxdioph  43402  expdiophlem2  43408  expdioph  43409  amgm3d  44584  stoweidlem26  46413  31prm  47986  lighneallem4b  47998  3odd  48097  sbgoldbo  48176  itcoval3  49054  ackval3  49072