Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Geometry in the Euclidean space
Properties relating betweenness and congruence
btwncolinear1
Next ⟩
btwncolinear2
Metamath Proof Explorer
Ascii
Unicode
Theorem
btwncolinear1
Description:
Betweenness implies colinearity.
(Contributed by
Scott Fenton
, 7-Oct-2013)
Ref
Expression
Assertion
btwncolinear1
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
→
C
Btwn
A
B
→
A
Colinear
B
C
Proof
Step
Hyp
Ref
Expression
1
3mix3
⊢
C
Btwn
A
B
→
A
Btwn
B
C
∨
B
Btwn
C
A
∨
C
Btwn
A
B
2
brcolinear
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
→
A
Colinear
B
C
↔
A
Btwn
B
C
∨
B
Btwn
C
A
∨
C
Btwn
A
B
3
1
2
syl5ibr
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
→
C
Btwn
A
B
→
A
Colinear
B
C