cgracol - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cgracol		Structured version Visualization version GIF version

Theorem cgracol 29194

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
cgracol	⊢ (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 class class class wbr 5111 ‘cfv 6540 (class class class)co 7419 ⟨“cs3 14907 Basecbs 17295 distcds 17345 TarskiGcstrkg 28751 Itvcitv 28757 LineGclng 28758 hlGchlg 28924 cgrAccgra 29173

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11175 ax-resscn 11176 ax-1cn 11177 ax-icn 11178 ax-addcl 11179 ax-addrcl 11180 ax-mulcl 11181 ax-mulrcl 11182 ax-mulcom 11183 ax-addass 11184 ax-mulass 11185 ax-distr 11186 ax-i2m1 11187 ax-1ne0 11188 ax-1rid 11189 ax-rnegex 11190 ax-rrecex 11191 ax-cnre 11192 ax-pre-lttri 11193 ax-pre-lttrn 11194 ax-pre-ltadd 11195 ax-pre-mulgt0 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-oadd 8463 df-er 8700 df-map 8832 df-pm 8833 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-dju 9903 df-card 9941 df-pnf 11264 df-mnf 11265 df-xr 11266 df-ltxr 11267 df-le 11268 df-sub 11462 df-neg 11463 df-nn 12253 df-2 12322 df-3 12323 df-n0 12524 df-xnn0 12597 df-z 12611 df-uz 12883 df-fz 13556 df-fzo 13704 df-hash 14389 df-word 14573 df-concat 14630 df-s1 14657 df-s2 14913 df-s3 14914 df-trkgc 28772 df-trkgb 28773 df-trkgcb 28774 df-trkg 28777 df-cgrg 28835 df-leg 28907 df-hlg 28925 df-cgra 29174

This theorem is used by: cgrancol 29195 tgasa1 29234

W3C validator