btwnlng13

Description: If Z is between X and Y , or Y is between X and Z , then Z lies on the line X Y . (Contributed by SS, 4-Jun-2026)

Step	Hyp	Ref	Expression
1		btwnlng13.p	$⊢ P = {Base}_{G}$
2		btwnlng13.i	$⊢ I = Itv (G)$
3		btwnlng13.l	$⊢ L = {Line}_{𝒢} (G)$
4		btwnlng13.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		btwnlng13.x	$⊢ φ \to X \in P$
6		btwnlng13.y	$⊢ φ \to Y \in P$
7		btwnlng13.z	$⊢ φ \to Z \in P$
8		btwnlng13.d	$⊢ φ \to X \neq Y$
9		btwnlng13.1	$⊢ φ \to (Z \in (X I Y) \lor Y \in (X I Z))$
10	4	adantr	$⊢ (φ \land Z \in (X I Y)) \to G \in 𝒢_{Tarski}$
11	5	adantr	$⊢ (φ \land Z \in (X I Y)) \to X \in P$
12	6	adantr	$⊢ (φ \land Z \in (X I Y)) \to Y \in P$
13	7	adantr	$⊢ (φ \land Z \in (X I Y)) \to Z \in P$
14	8	adantr	$⊢ (φ \land Z \in (X I Y)) \to X \neq Y$
15		simpr	$⊢ (φ \land Z \in (X I Y)) \to Z \in (X I Y)$
16	1 2 3 10 11 12 13 14 15	btwnlng1	$⊢ (φ \land Z \in (X I Y)) \to Z \in (X L Y)$
17	4	adantr	$⊢ (φ \land Y \in (X I Z)) \to G \in 𝒢_{Tarski}$
18	5	adantr	$⊢ (φ \land Y \in (X I Z)) \to X \in P$
19	6	adantr	$⊢ (φ \land Y \in (X I Z)) \to Y \in P$
20	7	adantr	$⊢ (φ \land Y \in (X I Z)) \to Z \in P$
21	8	adantr	$⊢ (φ \land Y \in (X I Z)) \to X \neq Y$
22		simpr	$⊢ (φ \land Y \in (X I Z)) \to Y \in (X I Z)$
23	1 2 3 17 18 19 20 21 22	btwnlng3	$⊢ (φ \land Y \in (X I Z)) \to Z \in (X L Y)$
24	16 23 9	mpjaodan	$⊢ φ \to Z \in (X L Y)$

Metamath Proof Explorer