Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltord2 Structured version   Unicode version

Theorem ltord2 9556
 Description: Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014.)
Hypotheses
Ref Expression
ltord.1
ltord.2
ltord.3
ltord.4
ltord.5
ltord2.6
Assertion
Ref Expression
ltord2
Distinct variable groups:   ,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   ()

Proof of Theorem ltord2
StepHypRef Expression
1 ltord.1 . . . 4
21negeqd 9300 . . 3
3 ltord.2 . . . 4
43negeqd 9300 . . 3
5 ltord.3 . . . 4
65negeqd 9300 . . 3
7 ltord.4 . . 3
8 ltord.5 . . . 4
98renegcld 9464 . . 3
10 ltord2.6 . . . 4
118ralrimiva 2789 . . . . . . 7
121eleq1d 2502 . . . . . . . 8
1312rspccva 3051 . . . . . . 7
1411, 13sylan 458 . . . . . 6
1514adantrl 697 . . . . 5
168adantrr 698 . . . . 5
17 ltneg 9528 . . . . 5
1815, 16, 17syl2anc 643 . . . 4
1910, 18sylibd 206 . . 3
202, 4, 6, 7, 9, 19ltord1 9553 . 2
215eleq1d 2502 . . . . . 6
2221rspccva 3051 . . . . 5
2311, 22sylan 458 . . . 4