Theorem btwnexch2

Description: Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of Schwabhauser p. 30. (Contributed by Scott Fenton, 14-Jun-2013)

	Ref	Expression
Assertion	btwnexch2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝐵 = 𝐶 → ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ↔ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
2	1	biimpd	⊢ ( 𝐵 = 𝐶 → ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
3	2	adantrd	⊢ ( 𝐵 = 𝐶 → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
4	3	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 = 𝐶 → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) )
5		simprl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) ) → 𝐵 ≠ 𝐶 )
6		simprr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )
7		btwnintr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
8	7	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
9	6 8	mpd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
10		simprrr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ )
11		btwnouttr2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
12	11	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) ) → ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
13	5 9 10 12	mp3and	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
14	13	exp32	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 ≠ 𝐶 → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) )
15	4 14	pm2.61dne	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )