Metamath Proof Explorer

Theorem btwnconn2

Description: Another connectivity law for betweenness. Theorem 5.2 of Schwabhauser p. 41. (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn2 
|- ( ( 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 <. B , D >. \/ D Btwn <. B , C >. ) ) )

Proof

Step Hyp Ref Expression
1 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 >. ) ) )
2 simpr2 
 |-  ( ( ( 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 >. ) ) -> B Btwn <. A , C >. )
3 2 anim1i 
 |-  ( ( ( ( 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 >. ) -> ( B Btwn <. A , C >. /\ C Btwn <. A , D >. ) )
4 btwnexch3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , D >. ) -> C Btwn <. B , D >. ) )
5 4 ad2antrr 
 |-  ( ( ( ( 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 >. ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , D >. ) -> C Btwn <. B , D >. ) )
6 3 5 mpd 
 |-  ( ( ( ( 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 >. ) -> C Btwn <. B , D >. )
7 6 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 >. -> C Btwn <. B , D >. ) )
8 simpr3 
 |-  ( ( ( 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 >. ) ) -> B Btwn <. A , D >. )
9 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
10 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
11 9 10 jca 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( D e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
12 btwnexch3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , D >. /\ D Btwn <. A , C >. ) -> D Btwn <. B , C >. ) )
13 11 12 syld3an3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , D >. /\ D Btwn <. A , C >. ) -> D Btwn <. B , C >. ) )
14 13 adantr 
 |-  ( ( ( 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 >. ) ) -> ( ( B Btwn <. A , D >. /\ D Btwn <. A , C >. ) -> D Btwn <. B , C >. ) )
15 8 14 mpand 
 |-  ( ( ( 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 >. ) ) -> ( D Btwn <. A , C >. -> D Btwn <. B , C >. ) )
16 7 15 orim12d 
 |-  ( ( ( 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 >. ) -> ( C Btwn <. B , D >. \/ D Btwn <. B , 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 >. ) -> ( C Btwn <. B , D >. \/ D Btwn <. B , C >. ) ) ) )
18 1 17 mpdd 
 |-  ( ( 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 <. B , D >. \/ D Btwn <. B , C >. ) ) )