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