Definition df-4 6118

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 6109	. 2 class 4
2		c3 6108	. . 3 class 3
3		c1 5389	. . 3 class 1
4		caddc 5391	. . 3 class +
5	2, 3, 4	co 4021	. 2 class (3 + 1)
6	1, 5	wceq 992	1 wff 4 = (3 + 1)

This definition is referenced by:  4re 6128  4pos 6138  2p2e4 6147  3p2e5 6153  4p4e8 6157  5p4e9 6160  6p4e10 6164  halfpm6th 6178  efaddlem20 7562  ef4pi 7607  sin01bndlem1 7676  sin01bndlem2 7677  ipval2 8611  sincosq4sgn 8974  sincos6thpi 8979  heiborlem32 12042

Copyright terms: Public domain