Definition df-3 12430

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 12422	. 2 class 3
2		c2 12421	. . 3 class 2
3		c1 11225	. . 3 class 1
4		caddc 11227	. . 3 class +
5	2, 3, 4	co 7440	. 2 class (2 + 1)
6	1, 5	wceq 1570	1 wff 3 = (2 + 1)

This definition is used by:  3nn  12446  3re  12447  3cn  12448  3m1e2  12494  2p2e4  12501  2p1e3  12508  3p3e6  12518  4p3e7  12520  5p3e8  12523  6p3e9  12526  3t3e9  12534  2lt3  12540  7p3e10  12918  7p6e13  12921  8p3e11  12924  8p5e13  12926  9p3e12  12931  9p4e13  12932  4t3e12  12941  5t3e15  12944  6t3e18  12948  7t3e21  12953  8t3e24  12959  9t3e27  12966  nn01to3  13092  fztpval  13744  fz0to3un2pr  13787  fzo0to42pr  13912  fzo1to4tp  13913  cu2  14367  i3  14371  binom3  14392  fac3  14448  hashtpg  14654  01sqrexlem7  15441  bpoly2  16249  bpoly4  16251  fsumcube  16252  ege2le3  16282  ef4p  16307  cos1bnd  16381  oddprmge3  16902  prmgaplem3  17257  13prm  17320  23prm  17323  43prm  17326  83prm  17327  163prm  17329  lt6abl  20136  cphipval  25591  vitalilem4  25959  itgcnlem  26137  dveflem  26326  sincosq3sgn  26856  sincosq4sgn  26857  tangtx  26861  sincos6thpi  26871  ang180lem2  27165  mcubic  27202  cubic2  27203  binom4  27205  dquartlem2  27207  quart1  27211  quartlem1  27212  log2ublem3  27303  basellem5  27439  basellem9  27443  ppi3  27525  cht3  27527  ppiublem1  27556  ppiublem2  27557  ppiub  27558  chtub  27566  bclbnd  27634  bposlem2  27639  bposlem9  27646  lgsdir2lem3  27681  dchrvmasumiflem1  27855  mulog2sumlem2  27889  pntlemk  27960  pntlemo  27961  axlowdimlem3  29549  axlowdimlem13  29559  axlowdimlem16  29562  axlowdimlem17  29563  2wlkdlem1  30541  elwwlks2s3  30567  elwspths2spth  30586  upgr3v3e3cycl  30808  upgr4cycl4dv4e  30813  konigsberglem5  30884  ipval2  31336  stm1add3i  32876  stadd3i  32877  problem2  36597  problem4  36599  sinccvglem  36603  mblfinlem3  38768  heiborlem6  38941  aks4d1p1  43317  2ap1caineq  43386  1p3e4  43501  nicomachus  43560  sn-0ne2  43648  3cubeslem2  43886  3cubeslem3r  43888  rmydioph  44212  rmxdioph  44214  expdiophlem2  44220  expdioph  44221  amgm3d  45389  stoweidlem26  47239  sin3t  48120  cos3t  48121  sin5tlem1  48122  goldpolyfactor  48130  2timesltsq  48651  2timesltsqm1  48652  31prm  48885  lighneallem4b  48897  nprmdvdsfacm1lem2  48909  3odd  49009  sbgoldbo  49088  itcoval3  49980  ackval3  49998