btwnexchand

Description: Deduction form of btwnexch . (Contributed by Scott Fenton, 13-Oct-2013)

Step	Hyp	Ref	Expression
1		btwnexchand.1	$⊢ φ \to N \in ℕ$
2		btwnexchand.2	$⊢ φ \to A \in 𝔼 (N)$
3		btwnexchand.3	$⊢ φ \to B \in 𝔼 (N)$
4		btwnexchand.4	$⊢ φ \to C \in 𝔼 (N)$
5		btwnexchand.5	$⊢ φ \to D \in 𝔼 (N)$
6		btwnexchand.6	$⊢ (φ \land ψ) \to B Btwn ⟨A, C⟩$
7		btwnexchand.7	$⊢ (φ \land ψ) \to C Btwn ⟨A, D⟩$
8		btwnexch	$⊢ (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 B Btwn ⟨A, D⟩)$
9	1 2 3 4 5 8	syl122anc	$⊢ φ \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, D⟩) \to B Btwn ⟨A, D⟩)$
10	9	adantr	$⊢ (φ \land ψ) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, D⟩) \to B Btwn ⟨A, D⟩)$
11	6 7 10	mp2and	$⊢ (φ \land ψ) \to B Btwn ⟨A, D⟩$

Metamath Proof Explorer