btwnexch3and

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

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

Metamath Proof Explorer