Metamath Proof Explorer


Theorem stle1

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

Ref Expression
Assertion stle1 S States A C S A 1

Proof

Step Hyp Ref Expression
1 sticl S States A C S A 0 1
2 elicc01 S A 0 1 S A 0 S A S A 1
3 2 simp3bi S A 0 1 S A 1
4 1 3 syl6 S States A C S A 1