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 ACBCCCABBC¬AC

Proof

Step Hyp Ref Expression
1 cvpss ACBCABAB
2 1 3adant3 ACBCCCABAB
3 cvpss BCCCBCBC
4 3 3adant1 ACBCCCBCBC
5 cvnbtwn ACCCBCAC¬ABBC
6 5 3com23 ACBCCCAC¬ABBC
7 6 con2d ACBCCCABBC¬AC
8 2 4 7 syl2and ACBCCCABBC¬AC