Definition df-3 5927

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 5918	. 2 class 3
2		c2 5917	. . 3 class 2
3		c1 5216	. . 3 class 1
4		caddc 5218	. . 3 class +
5	2, 3, 4	co 3955	. 2 class (2 + 1)
6	1, 5	wceq 954	1 wff 3 = (2 + 1)

This definition is referenced by:  3re 5937  3pos 5947  3nn 5956  2p2e4 5957  3p3e6 5964  4p3e7 5966  5p3e8 5969  6p3e9 5973  7p3e10 5976  3t3e9 5980  halfpm6th 5988  cu2 6580  i3 6672  fac3 6884  fsum4 6972  ele3lem 7277  ege2le3lem2 7280  efaddlem22 7310  ef4p 7349  cos1bnd 7425  sin01gt0 7427  cos01gt0 7428  ruclem1 7462  ruclem3 7464  ipval2 8305  sincosq3sgn 8644  sincosq4sgn 8645  sincos6thpi 8649  stm1add3 10114  stadd3 10115

Copyright terms: Public domain