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 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑃 OutsideOf ⟨ 𝐵 , 𝐶 ⟩ ) → 𝑃 OutsideOf ⟨ 𝐴 , 𝐶 ⟩ ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) → 𝐴 ≠ 𝑃 )
2 simplr ⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) → 𝐵 ≠ 𝑃 )
3 simprr ⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) → 𝐶 ≠ 𝑃 )
4 1 2 3 3jca ⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) → ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) )
5 simplr1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝐴 ≠ 𝑃 )
6 simplr3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → 𝐶 ≠ 𝑃 )
7 df-3an ⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) )
8 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
9 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
10 simp2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
11 simp2r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
12 simp3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
13 simpr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ )
14 simpr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ )
15 8 9 10 11 12 13 14 btwnexchand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ )
16 15 orcd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
17 7 16 sylan2br ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
18 17 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
19 simprlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ )
20 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ )
21 btwnconn3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
22 8 9 10 12 11 21 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
23 22 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
24 19 20 23 mp2and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
25 24 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
26 18 25 jaod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
27 26 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ → ( ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
28 simpll2 ⊢ ( ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) → 𝐵 ≠ 𝑃 )
29 28 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐵 ≠ 𝑃 )
30 29 necomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝑃 ≠ 𝐵 )
31 simprlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ )
32 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ )
33 btwnconn1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑃 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
34 8 9 11 10 12 33 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑃 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
35 34 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( ( 𝑃 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
36 30 31 32 35 mp3and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
37 36 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
38 df-3an ⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) )
39 simpr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ )
40 simpr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ )
41 8 9 12 11 10 39 40 btwnexchand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ )
42 41 olcd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
43 38 42 sylan2br ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
44 43 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
45 37 44 jaod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → ( ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
46 45 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) → ( 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ → ( ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
47 27 46 jaod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) → ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) → ( ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
48 47 imp32 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
49 5 6 48 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
50 49 exp31 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) → ( ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( 𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) ) )
51 4 50 syl5 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) → ( ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( 𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) ) )
52 51 impd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) → ( 𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
53 broutsideof2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
54 8 9 10 11 53 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
55 broutsideof2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) )
56 8 9 11 12 55 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) )
57 54 56 anbi12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑃 OutsideOf ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) ) )
58 df-3an ⊢ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ↔ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
59 df-3an ⊢ ( ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ↔ ( ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) )
60 58 59 anbi12i ⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ∧ ( ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) )
61 an4 ⊢ ( ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ∧ ( ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) )
62 60 61 bitr4i ⊢ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) )
63 57 62 bitrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑃 OutsideOf ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ) ) ∧ ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) ) )
64 broutsideof2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐶 ⟩ ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
65 8 9 10 12 64 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐶 ⟩ ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∨ 𝐶 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
66 52 63 65 3imtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑃 OutsideOf ⟨ 𝐵 , 𝐶 ⟩ ) → 𝑃 OutsideOf ⟨ 𝐴 , 𝐶 ⟩ ) )