Metamath Proof Explorer

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	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩) \to C Btwn ⟨A, D⟩)$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ B = C \to (B Btwn ⟨A, D⟩ \leftrightarrow C Btwn ⟨A, D⟩)$
2	1	biimpd	$⊢ B = C \to (B Btwn ⟨A, D⟩ \to C Btwn ⟨A, D⟩)$
3	2	adantrd	$⊢ B = C \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩) \to C Btwn ⟨A, D⟩)$
4	3	a1i	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (B = C \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩) \to C Btwn ⟨A, D⟩))$
5		simprl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩))) \to B \neq C$
6		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩))) \to (B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩)$
7		btwnintr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩) \to B Btwn ⟨A, C⟩)$
8	7	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩))) \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩) \to B Btwn ⟨A, C⟩)$
9	6 8	mpd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩))) \to B Btwn ⟨A, C⟩$
10		simprrr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩))) \to C Btwn ⟨B, D⟩$
11		btwnouttr2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \to C Btwn ⟨A, D⟩)$
12	11	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩))) \to ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \to C Btwn ⟨A, D⟩)$
13	5 9 10 12	mp3and	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land (B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩))) \to C Btwn ⟨A, D⟩$
14	13	exp32	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (B \neq C \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩) \to C Btwn ⟨A, D⟩))$
15	4 14	pm2.61dne	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B Btwn ⟨A, D⟩ \land C Btwn ⟨B, D⟩) \to C Btwn ⟨A, D⟩)$