Metamath Proof Explorer

Theorem btwnouttr

Description: Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of Schwabhauser p. 30. (Contributed by Scott Fenton, 14-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> N e. NN )
2 simp2r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
3 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
4 simp2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
5 necom 
 |-  ( B =/= C <-> C =/= B )
6 5 a1i 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( B =/= C <-> C =/= B ) )
7 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
8 btwncom 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) )
9 1 2 4 7 8 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) )
10 btwncom 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ B e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( C Btwn <. B , D >. <-> C Btwn <. D , B >. ) )
11 1 7 2 3 10 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( C Btwn <. B , D >. <-> C Btwn <. D , B >. ) )
12 6 9 11 3anbi123d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) <-> ( C =/= B /\ B Btwn <. C , A >. /\ C Btwn <. D , B >. ) ) )
13 3ancomb 
 |-  ( ( C =/= B /\ B Btwn <. C , A >. /\ C Btwn <. D , B >. ) <-> ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) )
14 12 13 syl6bb 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) <-> ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) ) )
15 14 biimpa 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) )
16 btwnouttr2 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) -> B Btwn <. D , A >. ) )
17 1 3 7 2 4 16 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) -> B Btwn <. D , A >. ) )
18 17 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> ( ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) -> B Btwn <. D , A >. ) )
19 15 18 mpd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> B Btwn <. D , A >. )
20 1 2 3 4 19 btwncomand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> B Btwn <. A , D >. )
21 20 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) -> B Btwn <. A , D >. ) )