Theorem btwnexch3and

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

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

Proof

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