Metamath Proof Explorer

Theorem btwnswapid

Description: If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwnswapid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC∧BBtwnAC→A=B

Proof

Step Hyp Ref Expression
1 simpl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→N∈ℕ
2 simpr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B∈𝔼⁡N
3 simpr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A∈𝔼⁡N
4 simpr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C∈𝔼⁡N
5 axpasch ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→ABtwnBC∧BBtwnAC→∃x∈𝔼⁡NxBtwnAA∧xBtwnBB
6 1 2 3 4 3 2 5 syl132anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC∧BBtwnAC→∃x∈𝔼⁡NxBtwnAA∧xBtwnBB
7 simpll ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→N∈ℕ
8 simpr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→x∈𝔼⁡N
9 simplr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→A∈𝔼⁡N
10 axbtwnid ⊢N∈ℕ∧x∈𝔼⁡N∧A∈𝔼⁡N→xBtwnAA→x=A
11 7 8 9 10 syl3anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→xBtwnAA→x=A
12 simplr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→B∈𝔼⁡N
13 axbtwnid ⊢N∈ℕ∧x∈𝔼⁡N∧B∈𝔼⁡N→xBtwnBB→x=B
14 7 8 12 13 syl3anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→xBtwnBB→x=B
15 11 14 anim12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→xBtwnAA∧xBtwnBB→x=A∧x=B
16 eqtr2 ⊢x=A∧x=B→A=B
17 15 16 syl6 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧x∈𝔼⁡N→xBtwnAA∧xBtwnBB→A=B
18 17 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∃x∈𝔼⁡NxBtwnAA∧xBtwnBB→A=B
19 6 18 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC∧BBtwnAC→A=B