Theorem cgracol

Description: Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020)

	Ref	Expression
Hypotheses	cgracol.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	cgracol.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	cgracol.m	⊢ − = ( dist ‘ 𝐺 )
	cgracol.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	cgracol.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	cgracol.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	cgracol.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	cgracol.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	cgracol.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	cgracol.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	cgracol.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
	cgracol.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	cgracol.2	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
Assertion	cgracol	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		cgracol.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		cgracol.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		cgracol.m	⊢ − = ( dist ‘ 𝐺 )
4		cgracol.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		cgracol.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		cgracol.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		cgracol.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		cgracol.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		cgracol.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10		cgracol.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11		cgracol.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
12		cgracol.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
13		cgracol.2	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
14	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐺 ∈ TarskiG )
15	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐴 ∈ 𝑃 )
16	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐵 ∈ 𝑃 )
17	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐶 ∈ 𝑃 )
18	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐷 ∈ 𝑃 )
19	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐸 ∈ 𝑃 )
20	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐹 ∈ 𝑃 )
21	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
22		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
23	1 2 22 4 5 6 7 8 9 10 11	cgrane2	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
24	23	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ≠ 𝐵 )
26	1 2 22 4 5 6 7 8 9 10 11	cgrane1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ≠ 𝐵 )
28	4	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
29	5	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
30	7	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ 𝑃 )
31	6	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
32		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) )
33	1 3 2 28 29 30 31 32	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) )
34	33	orcd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) )
35	25 27 34	3jca	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) )
36	24	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐶 ≠ 𝐵 )
37	26	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐴 ≠ 𝐵 )
38	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
39	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐶 ∈ 𝑃 )
40	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
41	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
42		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) )
43	1 3 2 38 39 40 41 42	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) )
44	43	olcd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) )
45	36 37 44	3jca	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) → ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) )
46	35 45	jaodan	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) )
47	1 2 22 7 5 6 4	ishlg	⊢ ( 𝜑 → ( 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) ) )
48	47	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ) ) ) )
49	46 48	mpbird	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 )
50	1 2 22 17 15 16 14 49	hlcomd	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 )
51	1 2 3 14 15 16 17 18 19 20 21 22 50	cgrahl	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 )
52	1 2 22 18 20 19 14	ishlg	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ↔ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) ) ) )
53	51 52	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) ) )
54	53	simp3d	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) )
55	4	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐺 ∈ TarskiG )
56	9	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐸 ∈ 𝑃 )
57	8	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐷 ∈ 𝑃 )
58	10	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐹 ∈ 𝑃 )
59		simpr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) )
60	1 3 2 55 56 57 58 59	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) )
61	60	olcd	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ) → ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ) )
62	4	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) → 𝐺 ∈ TarskiG )
63	9	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) → 𝐸 ∈ 𝑃 )
64	10	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) → 𝐹 ∈ 𝑃 )
65	8	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) → 𝐷 ∈ 𝑃 )
66		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) )
67	1 3 2 62 63 64 65 66	tgbtwncom	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) → 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) )
68	67	orcd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) → ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ) )
69	61 68	jaodan	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝐷 ) ) ) → ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ) )
70	54 69	syldan	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ) )
71	70	orcd	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ) ∨ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) )
72		df-3or	⊢ ( ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ∨ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) ↔ ( ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ) ∨ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) )
73	71 72	sylibr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ∨ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) )
74	1 2 4 22 5 6 7 8 9 10 11	cgracom	⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
75	1 2 22 4 8 9 10 5 6 7 74	cgrane1	⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
76	1 12 2 4 8 9 75 10	tgellng	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ↔ ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ∨ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) ) )
77	76	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ↔ ( 𝐹 ∈ ( 𝐷 𝐼 𝐸 ) ∨ 𝐷 ∈ ( 𝐹 𝐼 𝐸 ) ∨ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) ) )
78	73 77	mpbird	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) )
79	78	orcd	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
80	4	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
81	8	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐷 ∈ 𝑃 )
82	9	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐸 ∈ 𝑃 )
83	10	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐹 ∈ 𝑃 )
84	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
85	6	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ 𝑃 )
86	7	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
87	11	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
88		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
89	1 2 3 80 84 85 86 81 82 83 87 88	cgrabtwn	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
90	1 12 2 80 81 82 83 89	btwncolg3	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
91	26	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
92	13	orcomd	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) )
93	92	ord	⊢ ( 𝜑 → ( ¬ 𝐴 = 𝐵 → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) )
94	91 93	mpd	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
95	1 12 2 4 5 6 26 7	tgellng	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ↔ ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ) )
96	94 95	mpbid	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
97		df-3or	⊢ ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ↔ ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
98	96 97	sylib	⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ∨ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) ∨ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) )
99	79 90 98	mpjaodan	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )