Theorem tgbtwnexch3

Description: Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 18-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$$
	tgbtwnexch3.5	$$⊢\phi \to B\in \left(AIC\right)$$
	tgbtwnexch3.6	$$⊢\phi \to C\in \left(AID\right)$$
Assertion	tgbtwnexch3	$$⊢\phi \to C\in \left(BID\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		tgbtwnexch3.5	$$⊢\phi \to B\in \left(AIC\right)$$
10		tgbtwnexch3.6	$$⊢\phi \to C\in \left(AID\right)$$
11	1 2 3 4 5 6 7 9	tgbtwncom	$$⊢\phi \to B\in \left(CIA\right)$$
12	1 2 3 4 5 7 8 10	tgbtwncom	$$⊢\phi \to C\in \left(DIA\right)$$
13	1 2 3 4 6 7 8 5 11 12	tgbtwnintr	$$⊢\phi \to C\in \left(BID\right)$$