Definition df-3 6117

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

This definition is referenced by:  3re 6127  3pos 6137  3nn 6146  2p2e4 6147  3p3e6 6154  4p3e7 6156  5p3e8 6159  6p3e9 6163  7p3e10 6166  3t3e9 6170  halfpm6th 6178  cu2 6837  i3 6934  fac3 7141  fsum4 7228  ele3lem 7531  ege2le3lem2 7534  efaddlem22 7564  ef4pi 7607  cos1bnd 7683  sin01gt0 7685  cos01gt0 7686  ruclem1 7722  ruclem3 7724  ipval2 8611  sincosq3sgn 8973  sincosq4sgn 8974  sincos6thpi 8979  stm1add3i 10455  stadd3i 10456  heiborlem32 12042

Copyright terms: Public domain