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 
|- ( ph -> G e. TarskiG )
tgbtwnconn.a 
|- ( ph -> A e. P )
tgbtwnconn.b 
|- ( ph -> B e. P )
tgbtwnconn.c 
|- ( ph -> C e. P )
tgbtwnconn.d 
|- ( ph -> D e. P )
tgbtwnconn22.e 
|- ( ph -> E e. P )
tgbtwnconn22.1 
|- ( ph -> A =/= B )
tgbtwnconn22.2 
|- ( ph -> C =/= B )
tgbtwnconn22.3 
|- ( ph -> B e. ( A I C ) )
tgbtwnconn22.4 
|- ( ph -> B e. ( A I D ) )
tgbtwnconn22.5 
|- ( ph -> B e. ( C I E ) )
Assertion tgbtwnconn22 
|- ( ph -> B e. ( D I E ) )

Proof

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