Metamath Proof Explorer

Theorem btwnintr

Description: Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→N∈ℕ
2 simp2l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→A∈𝔼⁡N
3 simp2r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→B∈𝔼⁡N
4 simp3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→D∈𝔼⁡N
5 simp3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→C∈𝔼⁡N
6 axpasch ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧D∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAD∧CBtwnBD→∃x∈𝔼⁡NxBtwnBB∧xBtwnCA
7 1 2 3 4 3 5 6 syl132anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAD∧CBtwnBD→∃x∈𝔼⁡NxBtwnBB∧xBtwnCA
8 simpl1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→N∈ℕ
9 simpr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→x∈𝔼⁡N
10 simpl2r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→B∈𝔼⁡N
11 axbtwnid ⊢N∈ℕ∧x∈𝔼⁡N∧B∈𝔼⁡N→xBtwnBB→x=B
12 8 9 10 11 syl3anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→xBtwnBB→x=B
13 breq1 ⊢x=B→xBtwnCA↔BBtwnCA
14 13 biimpa ⊢x=B∧xBtwnCA→BBtwnCA
15 simpl3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→C∈𝔼⁡N
16 simpl2l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→A∈𝔼⁡N
17 btwncom ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→BBtwnCA↔BBtwnAC
18 8 10 15 16 17 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→BBtwnCA↔BBtwnAC
19 14 18 imbitrid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→x=B∧xBtwnCA→BBtwnAC
20 12 19 syland ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧x∈𝔼⁡N→xBtwnBB∧xBtwnCA→BBtwnAC
21 20 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∃x∈𝔼⁡NxBtwnBB∧xBtwnCA→BBtwnAC
22 7 21 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBtwnAD∧CBtwnBD→BBtwnAC