Metamath Proof Explorer


Theorem stge1i

Description: If a state is greater than or equal to 1, it is 1. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypothesis sto1.1 A C
Assertion stge1i S States 1 S A S A = 1

Proof

Step Hyp Ref Expression
1 sto1.1 A C
2 stle1 S States A C S A 1
3 1 2 mpi S States S A 1
4 3 anim1i S States 1 S A S A 1 1 S A
5 4 ex S States 1 S A S A 1 1 S A
6 stcl S States A C S A
7 1 6 mpi S States S A
8 1re 1
9 letri3 S A 1 S A = 1 S A 1 1 S A
10 7 8 9 sylancl S States S A = 1 S A 1 1 S A
11 5 10 sylibrd S States 1 S A S A = 1
12 1le1 1 1
13 breq2 S A = 1 1 S A 1 1
14 12 13 mpbiri S A = 1 1 S A
15 11 14 impbid1 S States 1 S A S A = 1