Definition df-3 7155

Description: Define the number 3.

Assertion

Ref	Expression
df-3	|- 3 = (2 + 1)

Detailed syntax breakdown of Definition df-3

Step	Hyp	Ref	Expression
1		c3 7146	. 2 class 3
2		c2 7145	. . 3 class 2
3		c1 6387	. . 3 class 1
4		caddc 6389	. . 3 class +
5	2, 3, 4	co 4884	. 2 class (2 + 1)
6	1, 5	wceq 1298	1 wff 3 = (2 + 1)

This definition is referenced by:  3re 7165  3pos 7175  3nn 7184  2p2e4 7185  3p3e6 7192  4p3e7 7194  5p3e8 7197  6p3e9 7201  7p3e10 7204  3t3e9 7208  2lt3 7213  halfpm6th 7218  fztpval 7688  cu2 7885  i3 7983  fac3 8190  fsum4 8285  ele3lem 8588  ege2le3lem2 8591  efaddlem22 8621  ef4pi 8664  cos1bnd 8740  sin01gt0 8742  cos01gt0 8743  ruclem1 8779  ruclem3 8781  ipval2 9696  sincosq3sgn 10055  sincosq4sgn 10056  sincos6thpi 10061  stm1add3i 11819  stadd3i 11820  3prm 13780  3timesi 14523  2eq3m1 14526  heiborlem32 15986  pcoass 16085  stb3xpl 16743

Copyright terms: Public domain