Definition df-3 12302

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 12294	. 2 class 3
2		c2 12293	. . 3 class 2
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7403	. 2 class (2 + 1)
6	1, 5	wceq 1540	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12317  3re  12318  3cn  12319  3pos  12343  3m1e2  12366  2p2e4  12373  2p1e3  12380  3p3e6  12390  4p3e7  12392  5p3e8  12395  6p3e9  12398  3t3e9  12405  2lt3  12410  7p3e10  12781  7p6e13  12784  8p3e11  12787  8p5e13  12789  9p3e12  12794  9p4e13  12795  4t3e12  12804  5t3e15  12807  6t3e18  12811  7t3e21  12816  8t3e24  12822  9t3e27  12829  nn01to3  12955  fztpval  13601  fz0to3un2pr  13644  fzo0to42pr  13767  fzo1to4tp  13768  cu2  14216  i3  14219  binom3  14240  fac3  14296  hashtpg  14501  01sqrexlem7  15265  bpoly2  16071  bpoly4  16073  fsumcube  16074  ege2le3  16104  ef4p  16129  cos1bnd  16203  oddprmge3  16717  prmgaplem3  17071  13prm  17133  23prm  17136  43prm  17139  83prm  17140  163prm  17142  lt6abl  19874  cphipval  25193  vitalilem4  25562  itgcnlem  25741  dveflem  25933  sincosq3sgn  26459  sincosq4sgn  26460  tangtx  26464  sincos6thpi  26475  ang180lem2  26770  mcubic  26807  cubic2  26808  binom4  26810  dquartlem2  26812  quart1  26816  quartlem1  26817  log2ublem3  26908  basellem5  27045  basellem8  27048  basellem9  27049  ppi3  27131  cht3  27133  ppiublem1  27163  ppiublem2  27164  ppiub  27165  chtub  27173  bclbnd  27241  bposlem2  27246  bposlem9  27253  lgsdir2lem3  27288  dchrvmasumiflem1  27462  mulog2sumlem2  27496  pntlemk  27567  pntlemo  27568  axlowdimlem3  28869  axlowdimlem13  28879  axlowdimlem16  28882  axlowdimlem17  28883  2wlkdlem1  29853  elwwlks2s3  29879  elwspths2spth  29895  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  konigsberglem5  30183  ipval2  30634  stm1add3i  32174  stadd3i  32175  problem2  35634  problem4  35636  sinccvglem  35640  mblfinlem3  37629  heiborlem6  37786  aks4d1p1  42035  2ap1caineq  42104  fac2xp3  42198  nicomachus  42308  sn-0ne2  42396  3cubeslem2  42655  3cubeslem3r  42657  rmydioph  42985  rmxdioph  42987  expdiophlem2  42993  expdioph  42994  amgm3d  44170  stoweidlem26  46003  31prm  47559  lighneallem4b  47571  3odd  47670  sbgoldbo  47749  itcoval3  48593  ackval3  48611