Theorem btwncomand

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

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

Proof

Step	Hyp	Ref	Expression
1		btwncomand.1	|- ( ph -> N e. NN )
2		btwncomand.2	|- ( ph -> A e. ( EE ` N ) )
3		btwncomand.3	|- ( ph -> B e. ( EE ` N ) )
4		btwncomand.4	|- ( ph -> C e. ( EE ` N ) )
5		btwncomand.5	|- ( ( ph /\ ps ) -> A Btwn <. B , C >. )
6		btwncom	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Btwn <. B , C >. <-> A Btwn <. C , B >. ) )
7	1 2 3 4 6	syl13anc	|- ( ph -> ( A Btwn <. B , C >. <-> A Btwn <. C , B >. ) )
8	7	adantr	|- ( ( ph /\ ps ) -> ( A Btwn <. B , C >. <-> A Btwn <. C , B >. ) )
9	5 8	mpbid	|- ( ( ph /\ ps ) -> A Btwn <. C , B >. )