Theorem cvnbtwn2

Description: The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	cvnbtwn2	|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A ( ( A C. C /\ C C_ B ) -> C = B ) ) )

Proof

Step	Hyp	Ref	Expression
1		cvnbtwn	|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A -. ( A C. C /\ C C. B ) ) )
2		iman	|- ( ( ( A C. C /\ C C_ B ) -> C = B ) <-> -. ( ( A C. C /\ C C_ B ) /\ -. C = B ) )
3		anass	|- ( ( ( A C. C /\ C C_ B ) /\ -. C = B ) <-> ( A C. C /\ ( C C_ B /\ -. C = B ) ) )
4		dfpss2	|- ( C C. B <-> ( C C_ B /\ -. C = B ) )
5	4	anbi2i	|- ( ( A C. C /\ C C. B ) <-> ( A C. C /\ ( C C_ B /\ -. C = B ) ) )
6	3 5	bitr4i	|- ( ( ( A C. C /\ C C_ B ) /\ -. C = B ) <-> ( A C. C /\ C C. B ) )
7	6	notbii	|- ( -. ( ( A C. C /\ C C_ B ) /\ -. C = B ) <-> -. ( A C. C /\ C C. B ) )
8	2 7	bitr2i	|- ( -. ( A C. C /\ C C. B ) <-> ( ( A C. C /\ C C_ B ) -> C = B ) )
9	1 8	imbitrdi	|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A ( ( A C. C /\ C C_ B ) -> C = B ) ) )