Metamath Proof Explorer

Theorem broutsideof3

Description: Characterization of outsideness in terms of relationship to a fourth point. Theorem 6.3 of Schwabhauser p. 43. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion broutsideof3 ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) )

Proof

Step Hyp Ref Expression
1 broutsideof2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
2 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
3 simpr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simpr1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
5 btwndiff ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) )
6 2 3 4 5 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) )
7 6 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) )
8 df-3an ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) )
9 3anass ⊢ ( ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ ( 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) )
10 simpr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝑃 ≠ 𝑐 )
11 10 necomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝑐 ≠ 𝑃 )
12 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
13 simp23 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
14 simp22 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
15 simp21 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
16 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simpr1r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ )
18 12 14 15 13 17 btwncomand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝐴 Btwn ⟨ 𝐵 , 𝑃 ⟩ )
19 simpr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ )
20 12 13 14 15 16 18 19 btwnexch3and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ )
21 11 20 19 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) )
22 8 9 21 syl2anbr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ∧ ( 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) ) → ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) )
23 22 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( ( 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) → ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
24 23 an32s ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) → ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
25 24 reximdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ( ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
26 7 25 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) )
27 26 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
28 simpr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
29 btwndiff ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) )
30 2 28 4 29 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) )
31 30 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) )
32 3anass ⊢ ( ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ↔ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) )
33 simpr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝑃 ≠ 𝑐 )
34 33 necomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝑐 ≠ 𝑃 )
35 simpr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ )
36 simpr1r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ )
37 12 13 15 14 36 btwncomand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝑃 ⟩ )
38 12 14 13 15 16 37 35 btwnexch3and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ )
39 34 35 38 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) → ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) )
40 8 32 39 syl2anbr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ∧ ( 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) ) ) → ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) )
41 40 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → ( ( 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) → ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
42 41 an32s ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) → ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
43 42 reximdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → ( ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 ≠ 𝑐 ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
44 31 43 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) )
45 44 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ) → ( 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
46 27 45 jaod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ) → ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
47 simprr1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) → 𝑐 ≠ 𝑃 )
48 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
49 simplr1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
50 simplr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
51 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) )
52 simprr2 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) → 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ )
53 48 49 50 51 52 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) → 𝑃 Btwn ⟨ 𝑐 , 𝐴 ⟩ )
54 simplr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
55 simprr3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) → 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ )
56 48 49 54 51 55 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) → 𝑃 Btwn ⟨ 𝑐 , 𝐵 ⟩ )
57 btwnconn2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝑐 , 𝐴 ⟩ ∧ 𝑃 Btwn ⟨ 𝑐 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
58 48 51 49 50 54 57 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝑐 , 𝐴 ⟩ ∧ 𝑃 Btwn ⟨ 𝑐 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
59 58 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) → ( ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝑐 , 𝐴 ⟩ ∧ 𝑃 Btwn ⟨ 𝑐 , 𝐵 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
60 47 53 56 59 mp3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) )
61 60 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ) → ( ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
62 61 an32s ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
63 62 rexlimdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ) → ( ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
64 46 63 impbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ) → ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ↔ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
65 64 pm5.32da ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ↔ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) )
66 df-3an ⊢ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ↔ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
67 df-3an ⊢ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ↔ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ) ∧ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) )
68 65 66 67 3bitr4g ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) )
69 1 68 bitrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨ 𝐴 , 𝑐 ⟩ ∧ 𝑃 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) ) ) )