Metamath Proof Explorer

Theorem btwnconn1

Description: Connectitivy law for betweenness. Theorem 5.1 of Schwabhauser p. 39-41. (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn1 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( B = C -> ( B Btwn <. A , D >. <-> C Btwn <. A , D >. ) )
2 1 3anbi3d 
 |-  ( B = C -> ( ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) <-> ( A =/= B /\ B Btwn <. A , C >. /\ C Btwn <. A , D >. ) ) )
3 orc 
 |-  ( C Btwn <. A , D >. -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) )
4 3 3ad2ant3 
 |-  ( ( A =/= B /\ B Btwn <. A , C >. /\ C Btwn <. A , D >. ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) )
5 2 4 syl6bi 
 |-  ( B = C -> ( ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) ) )
6 5 adantld 
 |-  ( B = C -> ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) ) )
7 simpr1 
 |-  ( ( B =/= C /\ ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) -> A =/= B )
8 simpl 
 |-  ( ( B =/= C /\ ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) -> B =/= C )
9 3simpc 
 |-  ( ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) -> ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) )
10 9 adantl 
 |-  ( ( B =/= C /\ ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) -> ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) )
11 7 8 10 jca31 
 |-  ( ( B =/= C /\ ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) -> ( ( A =/= B /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) )
12 btwnconn1lem14 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) )
13 11 12 sylan2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) )
14 13 an12s 
 |-  ( ( B =/= C /\ ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) )
15 14 ex 
 |-  ( B =/= C -> ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) ) )
16 6 15 pm2.61ine 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) )
17 16 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( A =/= B /\ B Btwn <. A , C >. /\ B Btwn <. A , D >. ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) ) )