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 AC
stle.2 BC
Assertion stlesi SStatesABSA=1SB=1

Proof

Step Hyp Ref Expression
1 stle.1 AC
2 stle.2 BC
3 stle1 SStatesBCSB1
4 2 3 mpi SStatesSB1
5 4 adantr SStatesABSA=1SB1
6 1 2 stlei SStatesABSASB
7 6 imp SStatesABSASB
8 7 adantrr SStatesABSA=1SASB
9 breq1 SA=1SASB1SB
10 9 ad2antll SStatesABSA=1SASB1SB
11 8 10 mpbid SStatesABSA=11SB
12 stcl SStatesBCSB
13 2 12 mpi SStatesSB
14 1re 1
15 13 14 jctir SStatesSB1
16 15 adantr SStatesABSA=1SB1
17 letri3 SB1SB=1SB11SB
18 16 17 syl SStatesABSA=1SB=1SB11SB
19 5 11 18 mpbir2and SStatesABSA=1SB=1
20 19 exp32 SStatesABSA=1SB=1