# 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 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({B}\mathrm{Btwn}⟨{A},{D}⟩\wedge {C}\mathrm{Btwn}⟨{B},{D}⟩\right)\to {B}\mathrm{Btwn}⟨{A},{C}⟩\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {N}\in ℕ$
2 simp2l ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {A}\in 𝔼\left({N}\right)$
3 simp2r ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {B}\in 𝔼\left({N}\right)$
4 simp3r ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {D}\in 𝔼\left({N}\right)$
5 simp3l ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {C}\in 𝔼\left({N}\right)$
6 axpasch ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\wedge \left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({B}\mathrm{Btwn}⟨{A},{D}⟩\wedge {C}\mathrm{Btwn}⟨{B},{D}⟩\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{Btwn}⟨{B},{B}⟩\wedge {x}\mathrm{Btwn}⟨{C},{A}⟩\right)\right)$
7 1 2 3 4 3 5 6 syl132anc ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({B}\mathrm{Btwn}⟨{A},{D}⟩\wedge {C}\mathrm{Btwn}⟨{B},{D}⟩\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{Btwn}⟨{B},{B}⟩\wedge {x}\mathrm{Btwn}⟨{C},{A}⟩\right)\right)$
8 simpl1 ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {N}\in ℕ$
9 simpr ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {x}\in 𝔼\left({N}\right)$
10 simpl2r ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {B}\in 𝔼\left({N}\right)$
11 axbtwnid ${⊢}\left({N}\in ℕ\wedge {x}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to \left({x}\mathrm{Btwn}⟨{B},{B}⟩\to {x}={B}\right)$
12 8 9 10 11 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left({x}\mathrm{Btwn}⟨{B},{B}⟩\to {x}={B}\right)$
13 breq1 ${⊢}{x}={B}\to \left({x}\mathrm{Btwn}⟨{C},{A}⟩↔{B}\mathrm{Btwn}⟨{C},{A}⟩\right)$
14 13 biimpa ${⊢}\left({x}={B}\wedge {x}\mathrm{Btwn}⟨{C},{A}⟩\right)\to {B}\mathrm{Btwn}⟨{C},{A}⟩$
15 simpl3l ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {C}\in 𝔼\left({N}\right)$
16 simpl2l ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {A}\in 𝔼\left({N}\right)$
17 btwncom ${⊢}\left({N}\in ℕ\wedge \left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\right)\to \left({B}\mathrm{Btwn}⟨{C},{A}⟩↔{B}\mathrm{Btwn}⟨{A},{C}⟩\right)$
18 8 10 15 16 17 syl13anc ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left({B}\mathrm{Btwn}⟨{C},{A}⟩↔{B}\mathrm{Btwn}⟨{A},{C}⟩\right)$
19 14 18 syl5ib ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left(\left({x}={B}\wedge {x}\mathrm{Btwn}⟨{C},{A}⟩\right)\to {B}\mathrm{Btwn}⟨{A},{C}⟩\right)$
20 12 19 syland ${⊢}\left(\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left(\left({x}\mathrm{Btwn}⟨{B},{B}⟩\wedge {x}\mathrm{Btwn}⟨{C},{A}⟩\right)\to {B}\mathrm{Btwn}⟨{A},{C}⟩\right)$
21 20 rexlimdva ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{Btwn}⟨{B},{B}⟩\wedge {x}\mathrm{Btwn}⟨{C},{A}⟩\right)\to {B}\mathrm{Btwn}⟨{A},{C}⟩\right)$
22 7 21 syld ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({B}\mathrm{Btwn}⟨{A},{D}⟩\wedge {C}\mathrm{Btwn}⟨{B},{D}⟩\right)\to {B}\mathrm{Btwn}⟨{A},{C}⟩\right)$