Definition df-3 12327

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 12319	. 2 class 3
2		c2 12318	. . 3 class 2
3		c1 11153	. . 3 class 1
4		caddc 11155	. . 3 class +
5	2, 3, 4	co 7430	. 2 class (2 + 1)
6	1, 5	wceq 1536	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12342  3re  12343  3cn  12344  3pos  12368  3m1e2  12391  2p2e4  12398  2p1e3  12405  3p3e6  12415  4p3e7  12417  5p3e8  12420  6p3e9  12423  3t3e9  12430  2lt3  12435  7p3e10  12805  7p6e13  12808  8p3e11  12811  8p5e13  12813  9p3e12  12818  9p4e13  12819  4t3e12  12828  5t3e15  12831  6t3e18  12835  7t3e21  12840  8t3e24  12846  9t3e27  12853  nn01to3  12980  fztpval  13622  fz0to3un2pr  13665  fzo0to42pr  13788  fzo1to4tp  13789  cu2  14235  i3  14238  binom3  14259  fac3  14315  hashtpg  14520  01sqrexlem7  15283  bpoly2  16089  bpoly4  16091  fsumcube  16092  ege2le3  16122  ef4p  16145  cos1bnd  16219  oddprmge3  16733  prmgaplem3  17086  13prm  17149  23prm  17152  43prm  17155  83prm  17156  163prm  17158  lt6abl  19927  cphipval  25290  vitalilem4  25659  itgcnlem  25839  dveflem  26031  sincosq3sgn  26556  sincosq4sgn  26557  tangtx  26561  sincos6thpi  26572  ang180lem2  26867  mcubic  26904  cubic2  26905  binom4  26907  dquartlem2  26909  quart1  26913  quartlem1  26914  log2ublem3  27005  basellem5  27142  basellem8  27145  basellem9  27146  ppi3  27228  cht3  27230  ppiublem1  27260  ppiublem2  27261  ppiub  27262  chtub  27270  bclbnd  27338  bposlem2  27343  bposlem9  27350  lgsdir2lem3  27385  dchrvmasumiflem1  27559  mulog2sumlem2  27593  pntlemk  27664  pntlemo  27665  axlowdimlem3  28973  axlowdimlem13  28983  axlowdimlem16  28986  axlowdimlem17  28987  2wlkdlem1  29954  elwwlks2s3  29980  elwspths2spth  29996  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  konigsberglem5  30284  ipval2  30735  stm1add3i  32275  stadd3i  32276  problem2  35650  problem4  35652  sinccvglem  35656  mblfinlem3  37645  heiborlem6  37802  aks4d1p1  42057  2ap1caineq  42126  fac2xp3  42220  nicomachus  42324  sn-0ne2  42412  3cubeslem2  42672  3cubeslem3r  42674  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  expdioph  43011  amgm3d  44188  stoweidlem26  45981  31prm  47521  lighneallem4b  47533  3odd  47632  sbgoldbo  47711  itcoval3  48514  ackval3  48532