Metamath Proof Explorer


Theorem tgbtwnconn22

Description: Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-2019)

Ref Expression
Hypotheses tgbtwnconn.p P = Base G
tgbtwnconn.i I = Itv G
tgbtwnconn.g φ G 𝒢 Tarski
tgbtwnconn.a φ A P
tgbtwnconn.b φ B P
tgbtwnconn.c φ C P
tgbtwnconn.d φ D P
tgbtwnconn22.e φ E P
tgbtwnconn22.1 φ A B
tgbtwnconn22.2 φ C B
tgbtwnconn22.3 φ B A I C
tgbtwnconn22.4 φ B A I D
tgbtwnconn22.5 φ B C I E
Assertion tgbtwnconn22 φ B D I E

Proof

Step Hyp Ref Expression
1 tgbtwnconn.p P = Base G
2 tgbtwnconn.i I = Itv G
3 tgbtwnconn.g φ G 𝒢 Tarski
4 tgbtwnconn.a φ A P
5 tgbtwnconn.b φ B P
6 tgbtwnconn.c φ C P
7 tgbtwnconn.d φ D P
8 tgbtwnconn22.e φ E P
9 tgbtwnconn22.1 φ A B
10 tgbtwnconn22.2 φ C B
11 tgbtwnconn22.3 φ B A I C
12 tgbtwnconn22.4 φ B A I D
13 tgbtwnconn22.5 φ B C I E
14 eqid dist G = dist G
15 3 adantr φ C B I D G 𝒢 Tarski
16 7 adantr φ C B I D D P
17 6 adantr φ C B I D C P
18 5 adantr φ C B I D B P
19 8 adantr φ C B I D E P
20 10 adantr φ C B I D C B
21 simpr φ C B I D C B I D
22 1 14 2 15 18 17 16 21 tgbtwncom φ C B I D C D I B
23 13 adantr φ C B I D B C I E
24 1 14 2 15 16 17 18 19 20 22 23 tgbtwnouttr2 φ C B I D B D I E
25 3 adantr φ D B I C G 𝒢 Tarski
26 7 adantr φ D B I C D P
27 5 adantr φ D B I C B P
28 8 adantr φ D B I C E P
29 6 adantr φ D B I C C P
30 simpr φ D B I C D B I C
31 13 adantr φ D B I C B C I E
32 1 14 2 25 29 27 28 31 tgbtwncom φ D B I C B E I C
33 1 14 2 25 26 27 28 29 30 32 tgbtwnintr φ D B I C B D I E
34 1 2 3 4 5 6 7 9 11 12 tgbtwnconn2 φ C B I D D B I C
35 24 33 34 mpjaodan φ B D I E