Description: A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tglineintmo.p | |
|
tglineintmo.i | |
||
tglineintmo.l | |
||
tglineintmo.g | |
||
coltr.a | |
||
coltr.b | |
||
coltr.c | |
||
coltr.d | |
||
coltr.1 | |
||
coltr3.2 | |
||
Assertion | coltr3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tglineintmo.p | |
|
2 | tglineintmo.i | |
|
3 | tglineintmo.l | |
|
4 | tglineintmo.g | |
|
5 | coltr.a | |
|
6 | coltr.b | |
|
7 | coltr.c | |
|
8 | coltr.d | |
|
9 | coltr.1 | |
|
10 | coltr3.2 | |
|
11 | eqid | |
|
12 | 4 | adantr | |
13 | 5 | adantr | |
14 | 8 | adantr | |
15 | 10 | adantr | |
16 | simpr | |
|
17 | 16 | oveq2d | |
18 | 15 17 | eleqtrrd | |
19 | 1 11 2 12 13 14 18 | axtgbtwnid | |
20 | 9 | adantr | |
21 | 19 20 | eqeltrrd | |
22 | 4 | adantr | |
23 | 5 | adantr | |
24 | 7 | adantr | |
25 | 8 | adantr | |
26 | simpr | |
|
27 | 10 | adantr | |
28 | 1 2 3 22 23 24 25 26 27 | btwnlng1 | |
29 | 26 | necomd | |
30 | 6 | adantr | |
31 | 1 3 2 4 6 7 9 | tglngne | |
32 | 31 | adantr | |
33 | 9 | adantr | |
34 | 1 2 3 22 24 23 30 29 33 32 | lnrot1 | |
35 | 1 2 3 22 24 23 29 30 32 34 | tglineelsb2 | |
36 | 1 2 3 22 23 24 26 | tglinecom | |
37 | 1 2 3 4 6 7 31 | tglinecom | |
38 | 37 | adantr | |
39 | 35 36 38 | 3eqtr4d | |
40 | 28 39 | eleqtrd | |
41 | 21 40 | pm2.61dane | |