Metamath Proof Explorer

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 = {Base}_{G}$
		tkgeom.d	$⊢ \underset{˙}{-} = dist (G)$
		tkgeom.i	$⊢ I = Itv (G)$
		tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
		tgbtwnintr.1	$⊢ φ \to A \in P$
		tgbtwnintr.2	$⊢ φ \to B \in P$
		tgbtwnintr.3	$⊢ φ \to C \in P$
		tgbtwnintr.4	$⊢ φ \to D \in P$
		tgbtwnexch.1	$⊢ φ \to B \in (A I C)$
		tgbtwnexch.2	$⊢ φ \to C \in (A I D)$
	Assertion	tgbtwnexch	$⊢ φ \to B \in (A I D)$

Proof

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