Metamath Proof Explorer

Theorem cvntr

Description: The covers relation is not transitive. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cvpss 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  A C. B ) )
2 1 3adant3 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A  A C. B ) )
3 cvpss 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B  B C. C ) )
4 3 3adant1 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( B  B C. C ) )
5 cvnbtwn 
 |-  ( ( A e. CH /\ C e. CH /\ B e. CH ) -> ( A  -. ( A C. B /\ B C. C ) ) )
6 5 3com23 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A  -. ( A C. B /\ B C. C ) ) )
7 6 con2d 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A C. B /\ B C. C ) -> -. A
8 2 4 7 syl2and 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A  -. A