Metamath Proof Explorer

Theorem btwncom

Description: Betweenness commutes. (Contributed by Scott Fenton, 12-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 btwncomim ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC→ABtwnCB
2 3ancomb ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N
3 btwncomim ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N→ABtwnCB→ABtwnBC
4 2 3 sylan2b ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnCB→ABtwnBC
5 1 4 impbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC↔ABtwnCB