Metamath Proof Explorer


Theorem cvnbtwn2

Description: The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvnbtwn2 ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝐵 → ( ( 𝐴𝐶𝐶𝐵 ) → 𝐶 = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cvnbtwn ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝐵 → ¬ ( 𝐴𝐶𝐶𝐵 ) ) )
2 iman ( ( ( 𝐴𝐶𝐶𝐵 ) → 𝐶 = 𝐵 ) ↔ ¬ ( ( 𝐴𝐶𝐶𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) )
3 anass ( ( ( 𝐴𝐶𝐶𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) ↔ ( 𝐴𝐶 ∧ ( 𝐶𝐵 ∧ ¬ 𝐶 = 𝐵 ) ) )
4 dfpss2 ( 𝐶𝐵 ↔ ( 𝐶𝐵 ∧ ¬ 𝐶 = 𝐵 ) )
5 4 anbi2i ( ( 𝐴𝐶𝐶𝐵 ) ↔ ( 𝐴𝐶 ∧ ( 𝐶𝐵 ∧ ¬ 𝐶 = 𝐵 ) ) )
6 3 5 bitr4i ( ( ( 𝐴𝐶𝐶𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) ↔ ( 𝐴𝐶𝐶𝐵 ) )
7 6 notbii ( ¬ ( ( 𝐴𝐶𝐶𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) ↔ ¬ ( 𝐴𝐶𝐶𝐵 ) )
8 2 7 bitr2i ( ¬ ( 𝐴𝐶𝐶𝐵 ) ↔ ( ( 𝐴𝐶𝐶𝐵 ) → 𝐶 = 𝐵 ) )
9 1 8 syl6ib ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝐵 → ( ( 𝐴𝐶𝐶𝐵 ) → 𝐶 = 𝐵 ) ) )