Metamath Proof Explorer


Theorem hlne1

Description: The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020)

Ref Expression
Hypotheses ishlg.p P=BaseG
ishlg.i I=ItvG
ishlg.k K=hl𝒢G
ishlg.a φAP
ishlg.b φBP
ishlg.c φCP
ishlg.g φGV
hlcomd.1 φAKCB
Assertion hlne1 φAC

Proof

Step Hyp Ref Expression
1 ishlg.p P=BaseG
2 ishlg.i I=ItvG
3 ishlg.k K=hl𝒢G
4 ishlg.a φAP
5 ishlg.b φBP
6 ishlg.c φCP
7 ishlg.g φGV
8 hlcomd.1 φAKCB
9 1 2 3 4 5 6 7 ishlg φAKCBACBCACIBBCIA
10 8 9 mpbid φACBCACIBBCIA
11 10 simp1d φAC