Definition df-4 5972

Description: Define the number 4.

Assertion

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

Detailed syntax breakdown of Definition df-4

Step	Hyp	Ref	Expression
1		c4 5963	. 2 class 4
2		c3 5962	. . 3 class 3
3		c1 5235	. . 3 class 1
4		caddc 5237	. . 3 class +
5	2, 3, 4	co 3963	. 2 class (3 + 1)
6	1, 5	wceq 956	1 wff 4 = (3 + 1)

This definition is referenced by:  4re 5982  4pos 5992  2p2e4 6001  3p2e5 6007  4p4e8 6011  5p4e9 6014  6p4e10 6018  halfpm6th 6032  efaddlem20 7357  ef4p 7399  sin01bndlem1 7467  sin01bndlem2 7468  ipval2 8357  sincosq4sgn 8707  sincos6thpi 8711

Copyright terms: Public domain