Metamath Proof Explorer


Theorem stlesi

Description: Ordering law for states. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses stle.1 A C
stle.2 B C
Assertion stlesi S States A B S A = 1 S B = 1

Proof

Step Hyp Ref Expression
1 stle.1 A C
2 stle.2 B C
3 stle1 S States B C S B 1
4 2 3 mpi S States S B 1
5 4 adantr S States A B S A = 1 S B 1
6 1 2 stlei S States A B S A S B
7 6 imp S States A B S A S B
8 7 adantrr S States A B S A = 1 S A S B
9 breq1 S A = 1 S A S B 1 S B
10 9 ad2antll S States A B S A = 1 S A S B 1 S B
11 8 10 mpbid S States A B S A = 1 1 S B
12 stcl S States B C S B
13 2 12 mpi S States S B
14 1re 1
15 13 14 jctir S States S B 1
16 15 adantr S States A B S A = 1 S B 1
17 letri3 S B 1 S B = 1 S B 1 1 S B
18 16 17 syl S States A B S A = 1 S B = 1 S B 1 1 S B
19 5 11 18 mpbir2and S States A B S A = 1 S B = 1
20 19 exp32 S States A B S A = 1 S B = 1