tgbtwnconnln3

Description: Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019)

Step	Hyp	Ref	Expression
1		tgbtwnconn.p	$⊢ P = {Base}_{G}$
2		tgbtwnconn.i	$⊢ I = Itv (G)$
3		tgbtwnconn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		tgbtwnconn.a	$⊢ φ \to A \in P$
5		tgbtwnconn.b	$⊢ φ \to B \in P$
6		tgbtwnconn.c	$⊢ φ \to C \in P$
7		tgbtwnconn.d	$⊢ φ \to D \in P$
8		tgbtwnconn3.1	$⊢ φ \to B \in (A I D)$
9		tgbtwnconn3.2	$⊢ φ \to C \in (A I D)$
10		tgbtwnconnln3.l	$⊢ L = {Line}_{𝒢} (G)$
11	3	adantr	$⊢ (φ \land B \in (A I C)) \to G \in 𝒢_{Tarski}$
12	4	adantr	$⊢ (φ \land B \in (A I C)) \to A \in P$
13	6	adantr	$⊢ (φ \land B \in (A I C)) \to C \in P$
14	5	adantr	$⊢ (φ \land B \in (A I C)) \to B \in P$
15		simpr	$⊢ (φ \land B \in (A I C)) \to B \in (A I C)$
16	1 10 2 11 12 13 14 15	btwncolg1	$⊢ (φ \land B \in (A I C)) \to (B \in (A L C) \lor A = C)$
17	3	adantr	$⊢ (φ \land C \in (A I B)) \to G \in 𝒢_{Tarski}$
18	4	adantr	$⊢ (φ \land C \in (A I B)) \to A \in P$
19	6	adantr	$⊢ (φ \land C \in (A I B)) \to C \in P$
20	5	adantr	$⊢ (φ \land C \in (A I B)) \to B \in P$
21		simpr	$⊢ (φ \land C \in (A I B)) \to C \in (A I B)$
22	1 10 2 17 18 19 20 21	btwncolg3	$⊢ (φ \land C \in (A I B)) \to (B \in (A L C) \lor A = C)$
23	1 2 3 4 5 6 7 8 9	tgbtwnconn3	$⊢ φ \to (B \in (A I C) \lor C \in (A I B))$
24	16 22 23	mpjaodan	$⊢ φ \to (B \in (A L C) \lor A = C)$

Metamath Proof Explorer