Metamath Proof Explorer

Theorem btwnexch

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

Ref Expression
Assertion btwnexch ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ∧ C Btwn A D → B Btwn A D

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → N ∈ ℕ
2 simp2r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
3 simp2l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
4 simp3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
5 btwncom ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B Btwn A C ↔ B Btwn C A
6 1 2 3 4 5 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ↔ B Btwn C A
7 simp3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
8 btwncom ⊢ N ∈ ℕ ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C Btwn A D ↔ C Btwn D A
9 1 4 3 7 8 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C Btwn A D ↔ C Btwn D A
10 6 9 anbi12d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ∧ C Btwn A D ↔ B Btwn C A ∧ C Btwn D A
11 ancom ⊢ B Btwn C A ∧ C Btwn D A ↔ C Btwn D A ∧ B Btwn C A
12 10 11 bitrdi ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ∧ C Btwn A D ↔ C Btwn D A ∧ B Btwn C A
13 btwnexch2 ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → C Btwn D A ∧ B Btwn C A → B Btwn D A
14 1 7 4 2 3 13 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C Btwn D A ∧ B Btwn C A → B Btwn D A
15 12 14 sylbid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ∧ C Btwn A D → B Btwn D A
16 btwncom ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B Btwn D A ↔ B Btwn A D
17 1 2 7 3 16 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn D A ↔ B Btwn A D
18 15 17 sylibd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ∧ C Btwn A D → B Btwn A D