Theorem tgbtwnouttr

Description: Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 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$$
	tgbtwnouttr.1	$$⊢\phi \to B\ne C$$
	tgbtwnouttr.2	$$⊢\phi \to B\in \left(AIC\right)$$
	tgbtwnouttr.3	$$⊢\phi \to C\in \left(BID\right)$$
Assertion	tgbtwnouttr	$$⊢\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		tgbtwnouttr.1	$$⊢\phi \to B\ne C$$
10		tgbtwnouttr.2	$$⊢\phi \to B\in \left(AIC\right)$$
11		tgbtwnouttr.3	$$⊢\phi \to C\in \left(BID\right)$$
12	9	necomd	$$⊢\phi \to C\ne B$$
13	1 2 3 4 6 7 8 11	tgbtwncom	$$⊢\phi \to C\in \left(DIB\right)$$
14	1 2 3 4 5 6 7 10	tgbtwncom	$$⊢\phi \to B\in \left(CIA\right)$$
15	1 2 3 4 8 7 6 5 12 13 14	tgbtwnouttr2	$$⊢\phi \to B\in \left(DIA\right)$$
16	1 2 3 4 8 6 5 15	tgbtwncom	$$⊢\phi \to B\in \left(AID\right)$$