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 27217

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 2733	. . . . . . . . . 10 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
21	1, 2, 20, 4, 6, 8, 10, 12, 14, 16, 18	cgrane2 27202	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
22	21	necomd 2994	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
23	22	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ≠ 𝐵)
24	1, 2, 20, 4, 6, 8, 10, 12, 14, 16, 18	cgrane1 27201	. . . . . . . . . . . . . . 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 26877	. . . . . . . . . . . . . . 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 26877	. . . . . . . . . . . . . . 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 26991	. . . . . . . . . . . . 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 26993	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐴((hlG‘𝐺)‘𝐵)𝐶)
49	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 19, 20, 48	cgrahl 27216	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐷((hlG‘𝐺)‘𝐸)𝐹)
50	1, 2, 20, 13, 17, 15, 5	ishlg 26991	. . . . . . . . 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 26877	. . . . . . . . 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 26877	. . . . . . . . 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 27211	. . . . . . 7 ⊢ (𝜑 → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
74	1, 2, 20, 4, 12, 14, 16, 6, 8, 10, 73	cgrane1 27201	. . . . . 6 ⊢ (𝜑 → 𝐷 ≠ 𝐸)
75	1, 72, 2, 4, 12, 14, 74, 16	tgellng 26942	. . . . 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 27215	. . 3 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ (𝐷𝐼𝐹))
89	1, 72, 2, 79, 80, 81, 82, 88	btwncolg3 26946	. 2 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
90	24	neneqd 2943	. . . . 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 26942	. . . 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 1537 ∈ wcel 2101 ≠ wne 2938 class class class wbr 5077 ‘cfv 6447 (class class class)co 7295 ⟨“cs3 14583 Basecbs 16940 distcds 16999 TarskiGcstrkg 26816 Itvcitv 26822 LineGclng 26823 hlGchlg 26989 cgrAccgra 27196

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-rep 5212 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7608 ax-cnex 10955 ax-resscn 10956 ax-1cn 10957 ax-icn 10958 ax-addcl 10959 ax-addrcl 10960 ax-mulcl 10961 ax-mulrcl 10962 ax-mulcom 10963 ax-addass 10964 ax-mulass 10965 ax-distr 10966 ax-i2m1 10967 ax-1ne0 10968 ax-1rid 10969 ax-rnegex 10970 ax-rrecex 10971 ax-cnre 10972 ax-pre-lttri 10973 ax-pre-lttrn 10974 ax-pre-ltadd 10975 ax-pre-mulgt0 10976

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3223 df-rab 3224 df-v 3436 df-sbc 3719 df-csb 3835 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3908 df-nul 4260 df-if 4463 df-pw 4538 df-sn 4565 df-pr 4567 df-tp 4569 df-op 4571 df-uni 4842 df-int 4883 df-iun 4929 df-br 5078 df-opab 5140 df-mpt 5161 df-tr 5195 df-id 5491 df-eprel 5497 df-po 5505 df-so 5506 df-fr 5546 df-we 5548 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-res 5603 df-ima 5604 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6399 df-fun 6449 df-fn 6450 df-f 6451 df-f1 6452 df-fo 6453 df-f1o 6454 df-fv 6455 df-riota 7252 df-ov 7298 df-oprab 7299 df-mpo 7300 df-om 7733 df-1st 7851 df-2nd 7852 df-frecs 8117 df-wrecs 8148 df-recs 8222 df-rdg 8261 df-1o 8317 df-oadd 8321 df-er 8518 df-map 8637 df-pm 8638 df-en 8754 df-dom 8755 df-sdom 8756 df-fin 8757 df-dju 9687 df-card 9725 df-pnf 11039 df-mnf 11040 df-xr 11041 df-ltxr 11042 df-le 11043 df-sub 11235 df-neg 11236 df-nn 12002 df-2 12064 df-3 12065 df-n0 12262 df-xnn0 12334 df-z 12348 df-uz 12611 df-fz 13268 df-fzo 13411 df-hash 14073 df-word 14246 df-concat 14302 df-s1 14329 df-s2 14589 df-s3 14590 df-trkgc 26837 df-trkgb 26838 df-trkgcb 26839 df-trkg 26842 df-cgrg 26900 df-leg 26972 df-hlg 26990 df-cgra 27197

This theorem is referenced by: cgrancol 27218 tgasa1 27247

W3C validator