Metamath Proof Explorer

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 = {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$
		tgbtwnexch3.5	$⊢ φ \to B \in (A I C)$
		tgbtwnexch3.6	$⊢ φ \to C \in (A I D)$
	Assertion	tgbtwnexch3	$⊢ φ \to C \in (B 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		tgbtwnexch3.5	$⊢ φ \to B \in (A I C)$
10		tgbtwnexch3.6	$⊢ φ \to C \in (A I D)$
11	1 2 3 4 5 6 7 9	tgbtwncom	$⊢ φ \to B \in (C I A)$
12	1 2 3 4 5 7 8 10	tgbtwncom	$⊢ φ \to C \in (D I A)$
13	1 2 3 4 6 7 8 5 11 12	tgbtwnintr	$⊢ φ \to C \in (B I D)$