# 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 ) ) )`