Definition df-3 5971

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 5962	. 2 class 3
2		c2 5961	. . 3 class 2
3		c1 5235	. . 3 class 1
4		caddc 5237	. . 3 class +
5	2, 3, 4	co 3963	. 2 class (2 + 1)
6	1, 5	wceq 956	1 wff 3 = (2 + 1)

This definition is referenced by:  3re 5981  3pos 5991  3nn 6000  2p2e4 6001  3p3e6 6008  4p3e7 6010  5p3e8 6013  6p3e9 6017  7p3e10 6020  3t3e9 6024  halfpm6th 6032  cu2 6640  i3 6733  fac3 6938  fsum4 7025  ele3lem 7326  ege2le3lem2 7329  efaddlem22 7359  ef4p 7399  cos1bnd 7474  sin01gt0 7476  cos01gt0 7477  ruclem1 7510  ruclem3 7512  ipval2 8357  sincosq3sgn 8706  sincosq4sgn 8707  sincos6thpi 8711  stm1add3 10174  stadd3 10175

Copyright terms: Public domain