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

Theorem ltord1 9545
 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
ltord.6
Assertion
Ref Expression
ltord1
Distinct variable groups:   ,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   ()

Proof of Theorem ltord1
StepHypRef Expression
1 ltord.1 . . 3
2 ltord.2 . . 3
3 ltord.3 . . 3
4 ltord.4 . . 3
5 ltord.5 . . 3
6 ltord.6 . . 3
71, 2, 3, 4, 5, 6ltordlem 9544 . 2
8 eqeq1 2441 . . . . . . . 8
92eqeq1d 2443 . . . . . . . 8
108, 9imbi12d 312 . . . . . . 7
1110, 3vtoclg 3003 . . . . . 6
1211ad2antrl 709 . . . . 5
131, 3, 2, 4, 5, 6ltordlem 9544 . . . . . 6
1413ancom2s 778 . . . . 5
1512, 14orim12d 812 . . . 4
1615con3d 127 . . 3
175ralrimiva 2781 . . . . . 6
182eleq1d 2501 . . . . . . 7
1918rspccva 3043 . . . . . 6
2017, 19sylan 458 . . . . 5
213eleq1d 2501 . . . . . . 7
2221rspccva 3043 . . . . . 6
2317, 22sylan 458 . . . . 5
2420, 23anim12dan 811 . . . 4
25 axlttri 9139 . . . 4
2624, 25syl 16 . . 3
274sseli 3336 . . . . 5
284sseli 3336 . . . . 5
29 axlttri 9139 . . . . 5
3027, 28, 29syl2an 464 . . . 4