Metamath Proof Explorer


Definition df-8

Description: Define the number 8. (Contributed by NM, 27-May-1999)

Ref Expression
Assertion df-8
|- 8 = ( 7 + 1 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c8
 |-  8
1 c7
 |-  7
2 caddc
 |-  +
3 c1
 |-  1
4 1 3 2 co
 |-  ( 7 + 1 )
5 0 4 wceq
 |-  8 = ( 7 + 1 )