Theorem tgbtwnexch

Description: Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 23-Mar-2019)

	Ref	Expression
Hypotheses	tkgeom.p	$$⊢P={\mathrm{Base}}_G$$
	tkgeom.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tkgeom.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tkgeom.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgbtwnintr.1	$$⊢\phi \to A\in P$$
	tgbtwnintr.2	$$⊢\phi \to B\in P$$
	tgbtwnintr.3	$$⊢\phi \to C\in P$$
	tgbtwnintr.4	$$⊢\phi \to D\in P$$
	tgbtwnexch.1	$$⊢\phi \to B\in \left(AIC\right)$$
	tgbtwnexch.2	$$⊢\phi \to C\in \left(AID\right)$$
Assertion	tgbtwnexch	$$⊢\phi \to B\in \left(AID\right)$$

Proof

Step	Hyp	Ref	Expression
1		tkgeom.p	$$⊢P={\mathrm{Base}}_G$$
2		tkgeom.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tkgeom.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tkgeom.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tgbtwnintr.1	$$⊢\phi \to A\in P$$
6		tgbtwnintr.2	$$⊢\phi \to B\in P$$
7		tgbtwnintr.3	$$⊢\phi \to C\in P$$
8		tgbtwnintr.4	$$⊢\phi \to D\in P$$
9		tgbtwnexch.1	$$⊢\phi \to B\in \left(AIC\right)$$
10		tgbtwnexch.2	$$⊢\phi \to C\in \left(AID\right)$$
11	1 2 3 4 5 7 8 10	tgbtwncom	$$⊢\phi \to C\in \left(DIA\right)$$
12	1 2 3 4 5 6 7 9	tgbtwncom	$$⊢\phi \to B\in \left(CIA\right)$$
13	1 2 3 4 8 7 6 5 11 12	tgbtwnexch2	$$⊢\phi \to B\in \left(DIA\right)$$
14	1 2 3 4 8 6 5 13	tgbtwncom	$$⊢\phi \to B\in \left(AID\right)$$