Metamath Proof Explorer


Theorem btwnexchand

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

Ref Expression
Hypotheses btwnexchand.1 φN
btwnexchand.2 φA𝔼N
btwnexchand.3 φB𝔼N
btwnexchand.4 φC𝔼N
btwnexchand.5 φD𝔼N
btwnexchand.6 φψBBtwnAC
btwnexchand.7 φψCBtwnAD
Assertion btwnexchand φψBBtwnAD

Proof

Step Hyp Ref Expression
1 btwnexchand.1 φN
2 btwnexchand.2 φA𝔼N
3 btwnexchand.3 φB𝔼N
4 btwnexchand.4 φC𝔼N
5 btwnexchand.5 φD𝔼N
6 btwnexchand.6 φψBBtwnAC
7 btwnexchand.7 φψCBtwnAD
8 btwnexch NA𝔼NB𝔼NC𝔼ND𝔼NBBtwnACCBtwnADBBtwnAD
9 1 2 3 4 5 8 syl122anc φBBtwnACCBtwnADBBtwnAD
10 9 adantr φψBBtwnACCBtwnADBBtwnAD
11 6 7 10 mp2and φψBBtwnAD