Definition df-4 5928

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

This definition is referenced by:  4re 5938  4pos 5948  2p2e4 5957  3p2e5 5963  4p4e8 5967  5p4e9 5970  6p4e10 5974  halfpm6th 5988  efaddlem20 7308  ef4p 7349  sin01bndlem1 7418  sin01bndlem2 7419  ipval2 8305  sincosq4sgn 8645  sincos6thpi 8649

Copyright terms: Public domain