Metamath Proof Explorer

Theorem btwnexch

Description: Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of Schwabhauser p. 30. (Contributed by Scott Fenton, 24-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→N∈ℕ
2 simp2r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→B∈𝔼⁡N
3 simp2l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→A∈𝔼⁡N
4 simp3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→C∈𝔼⁡N
5 btwncom ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC↔BBtwnCA
6 1 2 3 4 5 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAC↔BBtwnCA
7 simp3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→D∈𝔼⁡N
8 btwncom ⊢N∈ℕ∧C∈𝔼⁡N∧A∈𝔼⁡N∧D∈𝔼⁡N→CBtwnAD↔CBtwnDA
9 1 4 3 7 8 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→CBtwnAD↔CBtwnDA
10 6 9 anbi12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAC∧CBtwnAD↔BBtwnCA∧CBtwnDA
11 ancom ⊢BBtwnCA∧CBtwnDA↔CBtwnDA∧BBtwnCA
12 10 11 bitrdi ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAC∧CBtwnAD↔CBtwnDA∧BBtwnCA
13 btwnexch2 ⊢N∈ℕ∧D∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N∧A∈𝔼⁡N→CBtwnDA∧BBtwnCA→BBtwnDA
14 1 7 4 2 3 13 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→CBtwnDA∧BBtwnCA→BBtwnDA
15 12 14 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAC∧CBtwnAD→BBtwnDA
16 btwncom ⊢N∈ℕ∧B∈𝔼⁡N∧D∈𝔼⁡N∧A∈𝔼⁡N→BBtwnDA↔BBtwnAD
17 1 2 7 3 16 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnDA↔BBtwnAD
18 15 17 sylibd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAC∧CBtwnAD→BBtwnAD