Metamath Proof Explorer


Theorem stlei

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 stlei S States A B S A S B

Proof

Step Hyp Ref Expression
1 stle.1 A C
2 stle.2 B C
3 2 chshii B S
4 shococss B S B B
5 3 4 ax-mp B B
6 sstr2 A B B B A B
7 5 6 mpi A B A B
8 2 choccli B C
9 1 8 pm3.2i A C B C
10 7 9 jctil A B A C B C A B
11 stj S States A C B C A B S A B = S A + S B
12 10 11 syl5 S States A B S A B = S A + S B
13 12 imp S States A B S A B = S A + S B
14 1 8 chjcli A B C
15 stle1 S States A B C S A B 1
16 14 15 mpi S States S A B 1
17 2 sto1i S States S B + S B = 1
18 16 17 breqtrrd S States S A B S B + S B
19 18 adantr S States A B S A B S B + S B
20 13 19 eqbrtrrd S States A B S A + S B S B + S B
21 stcl S States A C S A
22 1 21 mpi S States S A
23 stcl S States B C S B
24 2 23 mpi S States S B
25 stcl S States B C S B
26 8 25 mpi S States S B
27 22 24 26 3jca S States S A S B S B
28 27 adantr S States A B S A S B S B
29 leadd1 S A S B S B S A S B S A + S B S B + S B
30 28 29 syl S States A B S A S B S A + S B S B + S B
31 20 30 mpbird S States A B S A S B
32 31 ex S States A B S A S B