Metamath Proof Explorer


Theorem cvnsym

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

Ref Expression
Assertion cvnsym ACBCAB¬BA

Proof

Step Hyp Ref Expression
1 cvpss ACBCABAB
2 cvpss BCACBABA
3 2 ancoms ACBCBABA
4 pssn2lp ¬BAAB
5 4 imnani BA¬AB
6 3 5 syl6 ACBCBA¬AB
7 6 con2d ACBCAB¬BA
8 1 7 syld ACBCAB¬BA