Metamath Proof Explorer


Theorem outsideofcom

Description: Commutitivity law for outsideness. Theorem 6.6 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideofcom N P 𝔼 N A 𝔼 N B 𝔼 N P OutsideOf A B P OutsideOf B A

Proof

Step Hyp Ref Expression
1 3ancoma A P B P A Btwn P B B Btwn P A B P A P A Btwn P B B Btwn P A
2 orcom A Btwn P B B Btwn P A B Btwn P A A Btwn P B
3 2 3anbi3i B P A P A Btwn P B B Btwn P A B P A P B Btwn P A A Btwn P B
4 1 3 bitri A P B P A Btwn P B B Btwn P A B P A P B Btwn P A A Btwn P B
5 4 a1i N P 𝔼 N A 𝔼 N B 𝔼 N A P B P A Btwn P B B Btwn P A B P A P B Btwn P A A Btwn P B
6 broutsideof2 N P 𝔼 N A 𝔼 N B 𝔼 N P OutsideOf A B A P B P A Btwn P B B Btwn P A
7 3ancomb P 𝔼 N A 𝔼 N B 𝔼 N P 𝔼 N B 𝔼 N A 𝔼 N
8 broutsideof2 N P 𝔼 N B 𝔼 N A 𝔼 N P OutsideOf B A B P A P B Btwn P A A Btwn P B
9 7 8 sylan2b N P 𝔼 N A 𝔼 N B 𝔼 N P OutsideOf B A B P A P B Btwn P A A Btwn P B
10 5 6 9 3bitr4d N P 𝔼 N A 𝔼 N B 𝔼 N P OutsideOf A B P OutsideOf B A