Metamath Proof Explorer

Theorem btwnconn2

Description: Another connectivity law for betweenness. Theorem 5.2 of Schwabhauser p. 41. (Contributed by Scott Fenton, 9-Oct-2013)

		Ref	Expression
	Assertion	btwnconn2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩) \to (C Btwn ⟨B, D⟩ \lor D Btwn ⟨B, C⟩))$

Proof

Step	Hyp	Ref	Expression
1		btwnconn1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩) \to (C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩))$
2		simpr2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to B Btwn ⟨A, C⟩$
3	2	anim1i	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land C Btwn ⟨A, D⟩) \to (B Btwn ⟨A, C⟩ \land C Btwn ⟨A, D⟩)$
4		btwnexch3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, D⟩) \to C Btwn ⟨B, D⟩)$
5	4	ad2antrr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land C Btwn ⟨A, D⟩) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, D⟩) \to C Btwn ⟨B, D⟩)$
6	3 5	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land C Btwn ⟨A, D⟩) \to C Btwn ⟨B, D⟩$
7	6	ex	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to (C Btwn ⟨A, D⟩ \to C Btwn ⟨B, D⟩)$
8		simpr3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to B Btwn ⟨A, D⟩$
9		simp3r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to D \in 𝔼 (N)$
10		simp3l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to C \in 𝔼 (N)$
11	9 10	jca	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (D \in 𝔼 (N) \land C \in 𝔼 (N))$
12		btwnexch3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((B Btwn ⟨A, D⟩ \land D Btwn ⟨A, C⟩) \to D Btwn ⟨B, C⟩)$
13	11 12	syld3an3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B Btwn ⟨A, D⟩ \land D Btwn ⟨A, C⟩) \to D Btwn ⟨B, C⟩)$
14	13	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to ((B Btwn ⟨A, D⟩ \land D Btwn ⟨A, C⟩) \to D Btwn ⟨B, C⟩)$
15	8 14	mpand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to (D Btwn ⟨A, C⟩ \to D Btwn ⟨B, C⟩)$
16	7 15	orim12d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \to ((C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩) \to (C Btwn ⟨B, D⟩ \lor D Btwn ⟨B, C⟩))$
17	16	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩) \to ((C Btwn ⟨A, D⟩ \lor D Btwn ⟨A, C⟩) \to (C Btwn ⟨B, D⟩ \lor D Btwn ⟨B, C⟩)))$
18	1 17	mpdd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((A \neq B \land B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩) \to (C Btwn ⟨B, D⟩ \lor D Btwn ⟨B, C⟩))$