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 ( ( 𝐴C𝐵C𝐶C ) → ( ( 𝐴 𝐵𝐵 𝐶 ) → ¬ 𝐴 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cvpss ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵𝐴𝐵 ) )
2 1 3adant3 ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝐵𝐴𝐵 ) )
3 cvpss ( ( 𝐵C𝐶C ) → ( 𝐵 𝐶𝐵𝐶 ) )
4 3 3adant1 ( ( 𝐴C𝐵C𝐶C ) → ( 𝐵 𝐶𝐵𝐶 ) )
5 cvnbtwn ( ( 𝐴C𝐶C𝐵C ) → ( 𝐴 𝐶 → ¬ ( 𝐴𝐵𝐵𝐶 ) ) )
6 5 3com23 ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝐶 → ¬ ( 𝐴𝐵𝐵𝐶 ) ) )
7 6 con2d ( ( 𝐴C𝐵C𝐶C ) → ( ( 𝐴𝐵𝐵𝐶 ) → ¬ 𝐴 𝐶 ) )
8 2 4 7 syl2and ( ( 𝐴C𝐵C𝐶C ) → ( ( 𝐴 𝐵𝐵 𝐶 ) → ¬ 𝐴 𝐶 ) )