Theorem btwnexch3and

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

	Ref	Expression
Hypotheses	btwnexch3and.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	btwnexch3and.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
	btwnexch3and.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
	btwnexch3and.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
	btwnexch3and.5	⊢ ( 𝜑 → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
	btwnexch3and.6	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
	btwnexch3and.7	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
Assertion	btwnexch3and	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		btwnexch3and.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		btwnexch3and.2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3		btwnexch3and.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
4		btwnexch3and.4	⊢ ( 𝜑 → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5		btwnexch3and.5	⊢ ( 𝜑 → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
6		btwnexch3and.6	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
7		btwnexch3and.7	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
8		btwnexch3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )
9	1 2 3 4 5 8	syl122anc	⊢ ( 𝜑 → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) )
11	6 7 10	mp2and	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ )