Metamath Proof Explorer

Theorem outsideoftr

Description: Transitivity law for outsideness. Theorem 6.7 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideoftr 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( P OutsideOf <. A , B >. /\ P OutsideOf <. B , C >. ) -> P OutsideOf <. A , C >. ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A =/= P /\ B =/= P ) /\ ( B =/= P /\ C =/= P ) ) -> A =/= P )
2 simplr 
 |-  ( ( ( A =/= P /\ B =/= P ) /\ ( B =/= P /\ C =/= P ) ) -> B =/= P )
3 simprr 
 |-  ( ( ( A =/= P /\ B =/= P ) /\ ( B =/= P /\ C =/= P ) ) -> C =/= P )
4 1 2 3 3jca 
 |-  ( ( ( A =/= P /\ B =/= P ) /\ ( B =/= P /\ C =/= P ) ) -> ( A =/= P /\ B =/= P /\ C =/= P ) )
5 simplr1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P /\ C =/= P ) ) /\ ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) -> A =/= P )
6 simplr3 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P /\ C =/= P ) ) /\ ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) -> C =/= P )
7 df-3an 
 |-  ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. /\ B Btwn <. P , C >. ) <-> ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. ) /\ B Btwn <. P , C >. ) )
8 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> N e. NN )
9 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> P e. ( EE ` N ) )
10 simp2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
11 simp2r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
12 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
13 simpr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. /\ B Btwn <. P , C >. ) ) -> A Btwn <. P , B >. )
14 simpr3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. /\ B Btwn <. P , C >. ) ) -> B Btwn <. P , C >. )
15 8 9 10 11 12 13 14 btwnexchand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. /\ B Btwn <. P , C >. ) ) -> A Btwn <. P , C >. )
16 15 orcd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. /\ B Btwn <. P , C >. ) ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) )
17 7 16 sylan2br 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. ) /\ B Btwn <. P , C >. ) ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) )
18 17 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. ) ) -> ( B Btwn <. P , C >. -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
19 simprlr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. ) /\ C Btwn <. P , B >. ) ) -> A Btwn <. P , B >. )
20 simprr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. ) /\ C Btwn <. P , B >. ) ) -> C Btwn <. P , B >. )
21 btwnconn3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( A Btwn <. P , B >. /\ C Btwn <. P , B >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
22 8 9 10 12 11 21 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( A Btwn <. P , B >. /\ C Btwn <. P , B >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
23 22 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. ) /\ C Btwn <. P , B >. ) ) -> ( ( A Btwn <. P , B >. /\ C Btwn <. P , B >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
24 19 20 23 mp2and 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. ) /\ C Btwn <. P , B >. ) ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) )
25 24 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. ) ) -> ( C Btwn <. P , B >. -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
26 18 25 jaod 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ A Btwn <. P , B >. ) ) -> ( ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
27 26 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P /\ C =/= P ) ) -> ( A Btwn <. P , B >. -> ( ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) ) )
28 simpll2 
 |-  ( ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) /\ B Btwn <. P , C >. ) -> B =/= P )
29 28 adantl 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) /\ B Btwn <. P , C >. ) ) -> B =/= P )
30 29 necomd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) /\ B Btwn <. P , C >. ) ) -> P =/= B )
31 simprlr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) /\ B Btwn <. P , C >. ) ) -> B Btwn <. P , A >. )
32 simprr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) /\ B Btwn <. P , C >. ) ) -> B Btwn <. P , C >. )
33 btwnconn1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( P =/= B /\ B Btwn <. P , A >. /\ B Btwn <. P , C >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
34 8 9 11 10 12 33 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( P =/= B /\ B Btwn <. P , A >. /\ B Btwn <. P , C >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
35 34 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) /\ B Btwn <. P , C >. ) ) -> ( ( P =/= B /\ B Btwn <. P , A >. /\ B Btwn <. P , C >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
36 30 31 32 35 mp3and 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) /\ B Btwn <. P , C >. ) ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) )
37 36 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) ) -> ( B Btwn <. P , C >. -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
38 df-3an 
 |-  ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. /\ C Btwn <. P , B >. ) <-> ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) /\ C Btwn <. P , B >. ) )
39 simpr3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. /\ C Btwn <. P , B >. ) ) -> C Btwn <. P , B >. )
40 simpr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. /\ C Btwn <. P , B >. ) ) -> B Btwn <. P , A >. )
41 8 9 12 11 10 39 40 btwnexchand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. /\ C Btwn <. P , B >. ) ) -> C Btwn <. P , A >. )
42 41 olcd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. /\ C Btwn <. P , B >. ) ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) )
43 38 42 sylan2br 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) /\ C Btwn <. P , B >. ) ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) )
44 43 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) ) -> ( C Btwn <. P , B >. -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
45 37 44 jaod 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( ( A =/= P /\ B =/= P /\ C =/= P ) /\ B Btwn <. P , A >. ) ) -> ( ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
46 45 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P /\ C =/= P ) ) -> ( B Btwn <. P , A >. -> ( ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) ) )
47 27 46 jaod 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P /\ C =/= P ) ) -> ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) -> ( ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) ) )
48 47 imp32 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P /\ C =/= P ) ) /\ ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) -> ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) )
49 5 6 48 3jca 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) /\ ( A =/= P /\ B =/= P /\ C =/= P ) ) /\ ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) -> ( A =/= P /\ C =/= P /\ ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) )
50 49 exp31 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( A =/= P /\ B =/= P /\ C =/= P ) -> ( ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) -> ( A =/= P /\ C =/= P /\ ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) ) ) )
51 4 50 syl5 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( ( A =/= P /\ B =/= P ) /\ ( B =/= P /\ C =/= P ) ) -> ( ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) -> ( A =/= P /\ C =/= P /\ ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) ) ) )
52 51 impd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( ( ( A =/= P /\ B =/= P ) /\ ( B =/= P /\ C =/= P ) ) /\ ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) -> ( A =/= P /\ C =/= P /\ ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) ) )
53 broutsideof2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
54 8 9 10 11 53 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) ) )
55 broutsideof2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( P OutsideOf <. B , C >. <-> ( B =/= P /\ C =/= P /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) )
56 8 9 11 12 55 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P OutsideOf <. B , C >. <-> ( B =/= P /\ C =/= P /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) )
57 54 56 anbi12d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( P OutsideOf <. A , B >. /\ P OutsideOf <. B , C >. ) <-> ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) /\ ( B =/= P /\ C =/= P /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) ) )
58 df-3an 
 |-  ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) <-> ( ( A =/= P /\ B =/= P ) /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) )
59 df-3an 
 |-  ( ( B =/= P /\ C =/= P /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) <-> ( ( B =/= P /\ C =/= P ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) )
60 58 59 anbi12i 
 |-  ( ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) /\ ( B =/= P /\ C =/= P /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) <-> ( ( ( A =/= P /\ B =/= P ) /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) /\ ( ( B =/= P /\ C =/= P ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) )
61 an4 
 |-  ( ( ( ( A =/= P /\ B =/= P ) /\ ( B =/= P /\ C =/= P ) ) /\ ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) <-> ( ( ( A =/= P /\ B =/= P ) /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) /\ ( ( B =/= P /\ C =/= P ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) )
62 60 61 bitr4i 
 |-  ( ( ( A =/= P /\ B =/= P /\ ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) ) /\ ( B =/= P /\ C =/= P /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) <-> ( ( ( A =/= P /\ B =/= P ) /\ ( B =/= P /\ C =/= P ) ) /\ ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) )
63 57 62 bitrdi 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( P OutsideOf <. A , B >. /\ P OutsideOf <. B , C >. ) <-> ( ( ( A =/= P /\ B =/= P ) /\ ( B =/= P /\ C =/= P ) ) /\ ( ( A Btwn <. P , B >. \/ B Btwn <. P , A >. ) /\ ( B Btwn <. P , C >. \/ C Btwn <. P , B >. ) ) ) ) )
64 broutsideof2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , C >. <-> ( A =/= P /\ C =/= P /\ ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) ) )
65 8 9 10 12 64 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , C >. <-> ( A =/= P /\ C =/= P /\ ( A Btwn <. P , C >. \/ C Btwn <. P , A >. ) ) ) )
66 52 63 65 3imtr4d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( P OutsideOf <. A , B >. /\ P OutsideOf <. B , C >. ) -> P OutsideOf <. A , C >. ) )