Metamath Proof Explorer


Theorem stge0

Description: The value of a state is nonnegative. (Contributed by NM, 24-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion stge0 SStatesAC0SA

Proof

Step Hyp Ref Expression
1 sticl SStatesACSA01
2 elicc01 SA01SA0SASA1
3 2 simp2bi SA010SA
4 1 3 syl6 SStatesAC0SA