Metamath Proof Explorer

Theorem btwnexch3and

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

Ref Expression
Hypotheses btwnexch3and.1 ⊢ φ → N ∈ ℕ
btwnexch3and.2 ⊢ φ → A ∈ 𝔼 ⁡ N
btwnexch3and.3 ⊢ φ → B ∈ 𝔼 ⁡ N
btwnexch3and.4 ⊢ φ → C ∈ 𝔼 ⁡ N
btwnexch3and.5 ⊢ φ → D ∈ 𝔼 ⁡ N
btwnexch3and.6 ⊢ φ ∧ ψ → B Btwn A C
btwnexch3and.7 ⊢ φ ∧ ψ → C Btwn A D
Assertion btwnexch3and ⊢ φ ∧ ψ → C Btwn B D

Proof

Step Hyp Ref Expression
1 btwnexch3and.1 ⊢ φ → N ∈ ℕ
2 btwnexch3and.2 ⊢ φ → A ∈ 𝔼 ⁡ N
3 btwnexch3and.3 ⊢ φ → B ∈ 𝔼 ⁡ N
4 btwnexch3and.4 ⊢ φ → C ∈ 𝔼 ⁡ N
5 btwnexch3and.5 ⊢ φ → D ∈ 𝔼 ⁡ N
6 btwnexch3and.6 ⊢ φ ∧ ψ → B Btwn A C
7 btwnexch3and.7 ⊢ φ ∧ ψ → C Btwn A D
8 btwnexch3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ∧ C Btwn A D → C Btwn B D
9 1 2 3 4 5 8 syl122anc ⊢ φ → B Btwn A C ∧ C Btwn A D → C Btwn B D
10 9 adantr ⊢ φ ∧ ψ → B Btwn A C ∧ C Btwn A D → C Btwn B D
11 6 7 10 mp2and ⊢ φ ∧ ψ → C Btwn B D