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 syl6bi N P 𝔼 N A 𝔼 N B 𝔼 N P OutsideOf A B B P