Description: Ordering law for states. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | stle.1 | |
|
stle.2 | |
||
Assertion | stlesi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stle.1 | |
|
2 | stle.2 | |
|
3 | stle1 | |
|
4 | 2 3 | mpi | |
5 | 4 | adantr | |
6 | 1 2 | stlei | |
7 | 6 | imp | |
8 | 7 | adantrr | |
9 | breq1 | |
|
10 | 9 | ad2antll | |
11 | 8 10 | mpbid | |
12 | stcl | |
|
13 | 2 12 | mpi | |
14 | 1re | |
|
15 | 13 14 | jctir | |
16 | 15 | adantr | |
17 | letri3 | |
|
18 | 16 17 | syl | |
19 | 5 11 18 | mpbir2and | |
20 | 19 | exp32 | |