Description: Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tgbtwnconn.p | |
|
tgbtwnconn.i | |
||
tgbtwnconn.g | |
||
tgbtwnconn.a | |
||
tgbtwnconn.b | |
||
tgbtwnconn.c | |
||
tgbtwnconn.d | |
||
tgbtwnconn3.1 | |
||
tgbtwnconn3.2 | |
||
tgbtwnconnln3.l | |
||
Assertion | tgbtwnconnln3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgbtwnconn.p | |
|
2 | tgbtwnconn.i | |
|
3 | tgbtwnconn.g | |
|
4 | tgbtwnconn.a | |
|
5 | tgbtwnconn.b | |
|
6 | tgbtwnconn.c | |
|
7 | tgbtwnconn.d | |
|
8 | tgbtwnconn3.1 | |
|
9 | tgbtwnconn3.2 | |
|
10 | tgbtwnconnln3.l | |
|
11 | 3 | adantr | |
12 | 4 | adantr | |
13 | 6 | adantr | |
14 | 5 | adantr | |
15 | simpr | |
|
16 | 1 10 2 11 12 13 14 15 | btwncolg1 | |
17 | 3 | adantr | |
18 | 4 | adantr | |
19 | 6 | adantr | |
20 | 5 | adantr | |
21 | simpr | |
|
22 | 1 10 2 17 18 19 20 21 | btwncolg3 | |
23 | 1 2 3 4 5 6 7 8 9 | tgbtwnconn3 | |
24 | 16 22 23 | mpjaodan | |