Metamath Proof Explorer

Theorem outsideofcom

Description: Commutativity 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