Definition df-3 12357

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 12349	. 2 class 3
2		c2 12348	. . 3 class 2
3		c1 11185	. . 3 class 1
4		caddc 11187	. . 3 class +
5	2, 3, 4	co 7448	. 2 class (2 + 1)
6	1, 5	wceq 1537	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12372  3re  12373  3cn  12374  3pos  12398  3m1e2  12421  2p2e4  12428  2p1e3  12435  3p3e6  12445  4p3e7  12447  5p3e8  12450  6p3e9  12453  3t3e9  12460  2lt3  12465  7p3e10  12833  7p6e13  12836  8p3e11  12839  8p5e13  12841  9p3e12  12846  9p4e13  12847  4t3e12  12856  5t3e15  12859  6t3e18  12863  7t3e21  12868  8t3e24  12874  9t3e27  12881  nn01to3  13006  fztpval  13646  fz0to3un2pr  13686  fzo0to42pr  13803  fzo1to4tp  13804  cu2  14249  i3  14252  binom3  14273  fac3  14329  hashtpg  14534  01sqrexlem7  15297  bpoly2  16105  bpoly4  16107  fsumcube  16108  ege2le3  16138  ef4p  16161  cos1bnd  16235  oddprmge3  16747  prmgaplem3  17100  13prm  17163  23prm  17166  43prm  17169  83prm  17170  163prm  17172  lt6abl  19937  cphipval  25296  vitalilem4  25665  itgcnlem  25845  dveflem  26037  sincosq3sgn  26560  sincosq4sgn  26561  tangtx  26565  sincos6thpi  26576  ang180lem2  26871  mcubic  26908  cubic2  26909  binom4  26911  dquartlem2  26913  quart1  26917  quartlem1  26918  log2ublem3  27009  basellem5  27146  basellem8  27149  basellem9  27150  ppi3  27232  cht3  27234  ppiublem1  27264  ppiublem2  27265  ppiub  27266  chtub  27274  bclbnd  27342  bposlem2  27347  bposlem9  27354  lgsdir2lem3  27389  dchrvmasumiflem1  27563  mulog2sumlem2  27597  pntlemk  27668  pntlemo  27669  axlowdimlem3  28977  axlowdimlem13  28987  axlowdimlem16  28990  axlowdimlem17  28991  2wlkdlem1  29958  elwwlks2s3  29984  elwspths2spth  30000  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  konigsberglem5  30288  ipval2  30739  stm1add3i  32279  stadd3i  32280  problem2  35634  problem4  35636  sinccvglem  35640  mblfinlem3  37619  heiborlem6  37776  aks4d1p1  42033  2ap1caineq  42102  fac2xp3  42196  nicomachus  42300  sn-0ne2  42382  3cubeslem2  42641  3cubeslem3r  42643  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  amgm3d  44161  stoweidlem26  45947  31prm  47471  lighneallem4b  47483  3odd  47582  sbgoldbo  47661  itcoval3  48399  ackval3  48417