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 27093

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 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐺 ∈ TarskiG)
6		cgracol.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
7	6	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐴 ∈ 𝑃)
8		cgracol.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
9	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ 𝑃)
10		cgracol.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
11	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐶 ∈ 𝑃)
12		cgracol.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
13	12	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐷 ∈ 𝑃)
14		cgracol.e	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
15	14	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐸 ∈ 𝑃)
16		cgracol.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
17	16	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐹 ∈ 𝑃)
18		cgracol.1	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
19	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
20		eqid 2738	. . . . . . . . . 10 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
21	1, 2, 20, 4, 6, 8, 10, 12, 14, 16, 18	cgrane2 27078	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
22	21	necomd 2998	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
23	22	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ≠ 𝐵)
24	1, 2, 20, 4, 6, 8, 10, 12, 14, 16, 18	cgrane1 27077	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
25	24	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐴 ≠ 𝐵)
26	4	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG)
27	6	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃)
28	10	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ 𝑃)
29	8	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃)
30		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐴𝐼𝐵))
31	1, 3, 2, 26, 27, 28, 29, 30	tgbtwncom 26753	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐵𝐼𝐴))
32	31	orcd 869	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))
33	23, 25, 32	3jca 1126	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
34	22	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶 ≠ 𝐵)
35	24	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ≠ 𝐵)
36	4	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐺 ∈ TarskiG)
37	10	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶 ∈ 𝑃)
38	6	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ 𝑃)
39	8	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐵 ∈ 𝑃)
40		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐶𝐼𝐵))
41	1, 3, 2, 36, 37, 38, 39, 40	tgbtwncom 26753	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐵𝐼𝐶))
42	41	olcd 870	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))
43	34, 35, 42	3jca 1126	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
44	33, 43	jaodan 954	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))
45	1, 2, 20, 10, 6, 8, 4	ishlg 26867	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶((hlG‘𝐺)‘𝐵)𝐴 ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
46	45	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐶((hlG‘𝐺)‘𝐵)𝐴 ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))))
47	44, 46	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐶((hlG‘𝐺)‘𝐵)𝐴)
48	1, 2, 20, 11, 7, 9, 5, 47	hlcomd 26869	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐴((hlG‘𝐺)‘𝐵)𝐶)
49	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 19, 20, 48	cgrahl 27092	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐷((hlG‘𝐺)‘𝐸)𝐹)
50	1, 2, 20, 13, 17, 15, 5	ishlg 26867	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷((hlG‘𝐺)‘𝐸)𝐹 ↔ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷)))))
51	49, 50	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷))))
52	51	simp3d 1142	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷)))
53	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐺 ∈ TarskiG)
54	14	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐸 ∈ 𝑃)
55	12	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ 𝑃)
56	16	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐹 ∈ 𝑃)
57		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ (𝐸𝐼𝐹))
58	1, 3, 2, 53, 54, 55, 56, 57	tgbtwncom 26753	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ (𝐹𝐼𝐸))
59	58	olcd 870	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
60	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐺 ∈ TarskiG)
61	14	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐸 ∈ 𝑃)
62	16	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ 𝑃)
63	12	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐷 ∈ 𝑃)
64		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ (𝐸𝐼𝐷))
65	1, 3, 2, 60, 61, 62, 63, 64	tgbtwncom 26753	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ (𝐷𝐼𝐸))
66	65	orcd 869	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
67	59, 66	jaodan 954	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
68	52, 67	syldan 590	. . . . . 6 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)))
69	68	orcd 869	. . . . 5 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))
70		df-3or 1086	. . . . 5 ⊢ ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹)) ↔ ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))
71	69, 70	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))
72		cgracol.l	. . . . . 6 ⊢ 𝐿 = (LineG‘𝐺)
73	1, 2, 4, 20, 6, 8, 10, 12, 14, 16, 18	cgracom 27087	. . . . . . 7 ⊢ (𝜑 → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
74	1, 2, 20, 4, 12, 14, 16, 6, 8, 10, 73	cgrane1 27077	. . . . . 6 ⊢ (𝜑 → 𝐷 ≠ 𝐸)
75	1, 72, 2, 4, 12, 14, 74, 16	tgellng 26818	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ↔ (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹))))
76	75	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐿𝐸) ↔ (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹))))
77	71, 76	mpbird 256	. . 3 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐹 ∈ (𝐷𝐿𝐸))
78	77	orcd 869	. 2 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
79	4	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐺 ∈ TarskiG)
80	12	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐷 ∈ 𝑃)
81	14	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ 𝑃)
82	16	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐹 ∈ 𝑃)
83	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐴 ∈ 𝑃)
84	8	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵 ∈ 𝑃)
85	10	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐶 ∈ 𝑃)
86	18	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
87		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵 ∈ (𝐴𝐼𝐶))
88	1, 2, 3, 79, 83, 84, 85, 80, 81, 82, 86, 87	cgrabtwn 27091	. . 3 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ (𝐷𝐼𝐹))
89	1, 72, 2, 79, 80, 81, 82, 88	btwncolg3 26822	. 2 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
90	24	neneqd 2947	. . . . 5 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
91		cgracol.2	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
92	91	orcomd 867	. . . . . 6 ⊢ (𝜑 → (𝐴 = 𝐵 ∨ 𝐶 ∈ (𝐴𝐿𝐵)))
93	92	ord 860	. . . . 5 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝐶 ∈ (𝐴𝐿𝐵)))
94	90, 93	mpd 15	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐿𝐵))
95	1, 72, 2, 4, 6, 8, 24, 10	tgellng 26818	. . . 4 ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶))))
96	94, 95	mpbid 231	. . 3 ⊢ (𝜑 → (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
97		df-3or 1086	. . 3 ⊢ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)) ↔ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
98	96, 97	sylib 217	. 2 ⊢ (𝜑 → ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))
99	78, 89, 98	mpjaodan 955	1 ⊢ (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∨ w3o 1084 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 ⟨“cs3 14483 Basecbs 16840 distcds 16897 TarskiGcstrkg 26693 Itvcitv 26699 LineGclng 26700 hlGchlg 26865 cgrAccgra 27072

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-oadd 8271 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-xnn0 12236 df-z 12250 df-uz 12512 df-fz 13169 df-fzo 13312 df-hash 13973 df-word 14146 df-concat 14202 df-s1 14229 df-s2 14489 df-s3 14490 df-trkgc 26713 df-trkgb 26714 df-trkgcb 26715 df-trkg 26718 df-cgrg 26776 df-leg 26848 df-hlg 26866 df-cgra 27073

This theorem is referenced by: cgrancol 27094 tgasa1 27123

W3C validator