Metamath Proof Explorer

Theorem btwncomim

Description: Betweenness commutes. Implication version. Theorem 3.2 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwncomim ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC→ABtwnCB

Proof

Step Hyp Ref Expression
1 btwntriv2 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAC
2 1 3adant3r2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAC
3 simpl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→N∈ℕ
4 simpr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B∈𝔼⁡N
5 simpr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A∈𝔼⁡N
6 simpr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C∈𝔼⁡N
7 axpasch ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC∧CBtwnAC→∃x∈𝔼⁡NxBtwnAA∧xBtwnCB
8 3 4 5 6 5 6 7 syl132anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC∧CBtwnAC→∃x∈𝔼⁡NxBtwnAA∧xBtwnCB
9 2 8 mpan2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC→∃x∈𝔼⁡NxBtwnAA∧xBtwnCB
10 simpll ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→N∈ℕ
11 simpr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→x∈𝔼⁡N
12 simplr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→A∈𝔼⁡N
13 axbtwnid ⊢N∈ℕ∧x∈𝔼⁡N∧A∈𝔼⁡N→xBtwnAA→x=A
14 10 11 12 13 syl3anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→xBtwnAA→x=A
15 breq1 ⊢x=A→xBtwnCB↔ABtwnCB
16 15 biimpd ⊢x=A→xBtwnCB→ABtwnCB
17 14 16 syl6 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→xBtwnAA→xBtwnCB→ABtwnCB
18 17 impd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→xBtwnAA∧xBtwnCB→ABtwnCB
19 18 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∃x∈𝔼⁡NxBtwnAA∧xBtwnCB→ABtwnCB
20 9 19 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC→ABtwnCB