Metamath Proof Explorer

Theorem outsidene2

Description: Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsidene2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P OutsideOf A B → B ≠ P

Proof

Step Hyp Ref Expression
1 broutsideof2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P OutsideOf A B ↔ A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A
2 simp2 ⊢ A ≠ P ∧ B ≠ P ∧ A Btwn P B ∨ B Btwn P A → B ≠ P
3 1 2 biimtrdi ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → P OutsideOf A B → B ≠ P