Metamath Proof Explorer

Theorem cvnbtwn3

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

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

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 ) -> A = C ) <-> -. ( ( A C_ C /\ C C. B ) /\ -. A = C ) )
3 eqcom 
 |-  ( C = A <-> A = C )
4 3 imbi2i 
 |-  ( ( ( A C_ C /\ C C. B ) -> C = A ) <-> ( ( A C_ C /\ C C. B ) -> A = C ) )
5 dfpss2 
 |-  ( A C. C <-> ( A C_ C /\ -. A = C ) )
6 5 anbi1i 
 |-  ( ( A C. C /\ C C. B ) <-> ( ( A C_ C /\ -. A = C ) /\ C C. B ) )
7 an32 
 |-  ( ( ( A C_ C /\ -. A = C ) /\ C C. B ) <-> ( ( A C_ C /\ C C. B ) /\ -. A = C ) )
8 6 7 bitri 
 |-  ( ( A C. C /\ C C. B ) <-> ( ( A C_ C /\ C C. B ) /\ -. A = C ) )
9 8 notbii 
 |-  ( -. ( A C. C /\ C C. B ) <-> -. ( ( A C_ C /\ C C. B ) /\ -. A = C ) )
10 2 4 9 3bitr4ri 
 |-  ( -. ( A C. C /\ C C. B ) <-> ( ( A C_ C /\ C C. B ) -> C = A ) )
11 1 10 syl6ib 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A  ( ( A C_ C /\ C C. B ) -> C = A ) ) )