Description: The half-line relation commutes. Theorem 6.6 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ishlg.p | |
|
ishlg.i | |
||
ishlg.k | |
||
ishlg.a | |
||
ishlg.b | |
||
ishlg.c | |
||
ishlg.g | |
||
Assertion | hlcomb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ishlg.p | |
|
2 | ishlg.i | |
|
3 | ishlg.k | |
|
4 | ishlg.a | |
|
5 | ishlg.b | |
|
6 | ishlg.c | |
|
7 | ishlg.g | |
|
8 | 3ancoma | |
|
9 | orcom | |
|
10 | 9 | a1i | |
11 | 10 | 3anbi3d | |
12 | 8 11 | syl5bb | |
13 | 1 2 3 4 5 6 7 | ishlg | |
14 | 1 2 3 5 4 6 7 | ishlg | |
15 | 12 13 14 | 3bitr4d | |