Definition df-3 11080

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 11071	. 2 class 3
2		c2 11070	. . 3 class 2
3		c1 9937	. . 3 class 1
4		caddc 9939	. . 3 class +
5	2, 3, 4	co 6650	. 2 class ( 2 + 1 )
6	1, 5	wceq 1483	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  11094  3pos  11114  3m1e2  11137  2p2e4  11144  2p1e3  11151  3p3e6  11161  4p3e7  11163  5p3e8  11166  6p3e9  11170  7p3e10OLD  11173  3t3e9  11180  3nn  11186  2lt3  11195  7p3e10  11603  7p6e13  11608  8p3e11  11612  8p3e11OLD  11613  8p5e13  11615  9p3e12  11621  9p4e13  11622  4t3e12  11632  5t3e15  11635  5t3e15OLD  11636  6t3e18  11642  7t3e21  11649  8t3e24  11655  9t3e27  11664  nn01to3  11781  fztpval  12402  fz0to3un2pr  12441  fz0to4untppr  12442  fzo0to42pr  12555  fzo1to4tp  12556  cu2  12963  i3  12966  binom3  12985  fac3  13067  hashtpg  13267  sqrlem7  13989  bpoly2  14788  bpoly4  14790  fsumcube  14791  ege2le3  14820  ef4p  14843  cos1bnd  14917  3prm  15406  oddprmge3  15412  prmgaplem3  15757  13prm  15823  23prm  15826  43prm  15829  83prm  15830  163prm  15832  lt6abl  18296  cphipval  23042  vitalilem4  23380  iblcnlem1  23554  itgcnlem  23556  dveflem  23742  sincosq3sgn  24252  sincosq4sgn  24253  tangtx  24257  sincos6thpi  24267  ang180lem2  24540  mcubic  24574  cubic2  24575  binom4  24577  dquartlem2  24579  quart1  24583  quartlem1  24584  log2ublem3  24675  basellem5  24811  basellem8  24814  basellem9  24815  ppi3  24897  cht3  24899  ppiublem1  24927  ppiublem2  24928  ppiub  24929  chtub  24937  bclbnd  25005  bposlem2  25010  bposlem9  25017  lgsdir2lem3  25052  dchrvmasumiflem1  25190  mulog2sumlem2  25224  pntlemk  25295  pntlemo  25296  axlowdimlem3  25824  axlowdimlem13  25834  axlowdimlem16  25837  axlowdimlem17  25838  2wlkdlem1  26821  elwwlks2s3  26859  elwspths2spth  26862  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  konigsberglem5  27118  ipval2  27562  stm1add3i  29106  stadd3i  29107  problem2  31559  problem2OLD  31560  problem4  31562  sinccvglem  31566  mblfinlem3  33448  heiborlem6  33615  rmydioph  37581  rmxdioph  37583  expdiophlem2  37589  expdioph  37590  amgm3d  38502  stoweidlem26  40243  31prm  41512  lighneallem4b  41526  3odd  41617  sbgoldbo  41675