Theorem btwnexchand

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

	Ref	Expression
Hypotheses	btwnexchand.1	|- ( ph -> N e. NN )
	btwnexchand.2	|- ( ph -> A e. ( EE ` N ) )
	btwnexchand.3	|- ( ph -> B e. ( EE ` N ) )
	btwnexchand.4	|- ( ph -> C e. ( EE ` N ) )
	btwnexchand.5	|- ( ph -> D e. ( EE ` N ) )
	btwnexchand.6	|- ( ( ph /\ ps ) -> B Btwn <. A , C >. )
	btwnexchand.7	|- ( ( ph /\ ps ) -> C Btwn <. A , D >. )
Assertion	btwnexchand	|- ( ( ph /\ ps ) -> B Btwn <. A , D >. )

Proof

Step	Hyp	Ref	Expression
1		btwnexchand.1	|- ( ph -> N e. NN )
2		btwnexchand.2	|- ( ph -> A e. ( EE ` N ) )
3		btwnexchand.3	|- ( ph -> B e. ( EE ` N ) )
4		btwnexchand.4	|- ( ph -> C e. ( EE ` N ) )
5		btwnexchand.5	|- ( ph -> D e. ( EE ` N ) )
6		btwnexchand.6	|- ( ( ph /\ ps ) -> B Btwn <. A , C >. )
7		btwnexchand.7	|- ( ( ph /\ ps ) -> C Btwn <. A , D >. )
8		btwnexch	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , D >. ) -> B Btwn <. A , D >. ) )
9	1 2 3 4 5 8	syl122anc	|- ( ph -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , D >. ) -> B Btwn <. A , D >. ) )
10	9	adantr	|- ( ( ph /\ ps ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , D >. ) -> B Btwn <. A , D >. ) )
11	6 7 10	mp2and	|- ( ( ph /\ ps ) -> B Btwn <. A , D >. )