This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cvpss | |- ( ( A e. CH /\ B e. CH ) -> ( A |
|
| 2 | 1 | 3adant3 | |- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A |
| 3 | cvpss | |- ( ( B e. CH /\ C e. CH ) -> ( B |
|
| 4 | 3 | 3adant1 | |- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( B |
| 5 | cvnbtwn | |- ( ( A e. CH /\ C e. CH /\ B e. CH ) -> ( A |
|
| 6 | 5 | 3com23 | |- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A |
| 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 |