Metamath Proof Explorer

Theorem btwnexch3

Description: Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwnexch3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAC∧CBtwnAD→CBtwnBD

Proof

Step Hyp Ref Expression
1 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→N∈ℕ
2 simp3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→C∈𝔼⁡N
3 simp2l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→A∈𝔼⁡N
4 simp3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→D∈𝔼⁡N
5 btwncom ⊢N∈ℕ∧C∈𝔼⁡N∧A∈𝔼⁡N∧D∈𝔼⁡N→CBtwnAD↔CBtwnDA
6 1 2 3 4 5 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→CBtwnAD↔CBtwnDA
7 simp2r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→B∈𝔼⁡N
8 btwncom ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC↔BBtwnCA
9 1 7 3 2 8 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAC↔BBtwnCA
10 6 9 anbi12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→CBtwnAD∧BBtwnAC↔CBtwnDA∧BBtwnCA
11 axpasch ⊢N∈ℕ∧D∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N→CBtwnDA∧BBtwnCA→∃x∈𝔼⁡NxBtwnCC∧xBtwnBD
12 1 4 2 3 2 7 11 syl132anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→CBtwnDA∧BBtwnCA→∃x∈𝔼⁡NxBtwnCC∧xBtwnBD
13 10 12 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→CBtwnAD∧BBtwnAC→∃x∈𝔼⁡NxBtwnCC∧xBtwnBD
14 13 ancomsd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAC∧CBtwnAD→∃x∈𝔼⁡NxBtwnCC∧xBtwnBD
15 simpl1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→N∈ℕ
16 simpr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→x∈𝔼⁡N
17 simpl3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→C∈𝔼⁡N
18 axbtwnid ⊢N∈ℕ∧x∈𝔼⁡N∧C∈𝔼⁡N→xBtwnCC→x=C
19 15 16 17 18 syl3anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→xBtwnCC→x=C
20 breq1 ⊢x=C→xBtwnBD↔CBtwnBD
21 20 biimpd ⊢x=C→xBtwnBD→CBtwnBD
22 19 21 syl6 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→xBtwnCC→xBtwnBD→CBtwnBD
23 22 impd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→xBtwnCC∧xBtwnBD→CBtwnBD
24 23 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∃x∈𝔼⁡NxBtwnCC∧xBtwnBD→CBtwnBD
25 14 24 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAC∧CBtwnAD→CBtwnBD