btwnconn1lem11

Description: Lemma for btwnconn1 . Now, we establish that D and Q are equidistant from C . (Contributed by Scott Fenton, 8-Oct-2013)

		Ref	Expression
	Assertion	btwnconn1lem11	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨D, C⟩ Cgr ⟨Q, C⟩$

Proof

Step	Hyp	Ref	Expression
1		btwnconn1lem8	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨R, P⟩ Cgr ⟨E, d⟩$
2		btwnconn1lem9	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨R, Q⟩ Cgr ⟨E, D⟩$
3		btwnconn1lem10	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, D⟩ Cgr ⟨P, Q⟩$
4	1 2 3	3jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)$
5	4	adantr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \land d = E) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)$
6		simpr3r	$⊢ ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))) \to ⟨R, Q⟩ Cgr ⟨R, P⟩$
7	6	adantl	$⊢ ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to ⟨R, Q⟩ Cgr ⟨R, P⟩$
8		simpr2r	$⊢ ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))) \to ⟨C, R⟩ Cgr ⟨C, E⟩$
9	8	adantl	$⊢ ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to ⟨C, R⟩ Cgr ⟨C, E⟩$
10	7 9	jca	$⊢ ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to (⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩)$
11		opeq2	$⊢ d = E \to ⟨C, d⟩ = ⟨C, E⟩$
12	11	breq2d	$⊢ d = E \to (⟨C, R⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨C, R⟩ Cgr ⟨C, E⟩)$
13	12	anbi2d	$⊢ d = E \to ((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \leftrightarrow (⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩))$
14		opeq1	$⊢ d = E \to ⟨d, d⟩ = ⟨E, d⟩$
15	14	breq2d	$⊢ d = E \to (⟨R, P⟩ Cgr ⟨d, d⟩ \leftrightarrow ⟨R, P⟩ Cgr ⟨E, d⟩)$
16		opeq1	$⊢ d = E \to ⟨d, D⟩ = ⟨E, D⟩$
17	16	breq2d	$⊢ d = E \to (⟨R, Q⟩ Cgr ⟨d, D⟩ \leftrightarrow ⟨R, Q⟩ Cgr ⟨E, D⟩)$
18	15 17	3anbi12d	$⊢ d = E \to ((⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩) \leftrightarrow (⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩))$
19	13 18	anbi12d	$⊢ d = E \to (((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \land (⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \leftrightarrow ((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)))$
20	19	biimpar	$⊢ (d = E \land ((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩))) \to ((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \land (⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩))$
21		simpr1	$⊢ ((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \land (⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to ⟨R, P⟩ Cgr ⟨d, d⟩$
22		simp11	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to N \in ℕ$
23		simp33	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to R \in 𝔼 (N)$
24		simp31	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to P \in 𝔼 (N)$
25		simp2r1	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to d \in 𝔼 (N)$
26		axcgrid	$⊢ (N \in ℕ \land (R \in 𝔼 (N) \land P \in 𝔼 (N) \land d \in 𝔼 (N))) \to (⟨R, P⟩ Cgr ⟨d, d⟩ \to R = P)$
27	22 23 24 25 26	syl13anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨R, P⟩ Cgr ⟨d, d⟩ \to R = P)$
28	21 27	syl5	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \land (⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to R = P)$
29		opeq1	$⊢ R = P \to ⟨R, Q⟩ = ⟨P, Q⟩$
30		opeq1	$⊢ R = P \to ⟨R, P⟩ = ⟨P, P⟩$
31	29 30	breq12d	$⊢ R = P \to (⟨R, Q⟩ Cgr ⟨R, P⟩ \leftrightarrow ⟨P, Q⟩ Cgr ⟨P, P⟩)$
32		opeq2	$⊢ R = P \to ⟨C, R⟩ = ⟨C, P⟩$
33	32	breq1d	$⊢ R = P \to (⟨C, R⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨C, P⟩ Cgr ⟨C, d⟩)$
34	31 33	anbi12d	$⊢ R = P \to ((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \leftrightarrow (⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩))$
35	30	breq1d	$⊢ R = P \to (⟨R, P⟩ Cgr ⟨d, d⟩ \leftrightarrow ⟨P, P⟩ Cgr ⟨d, d⟩)$
36	29	breq1d	$⊢ R = P \to (⟨R, Q⟩ Cgr ⟨d, D⟩ \leftrightarrow ⟨P, Q⟩ Cgr ⟨d, D⟩)$
37	35 36	3anbi12d	$⊢ R = P \to ((⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩) \leftrightarrow (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩))$
38	34 37	anbi12d	$⊢ R = P \to (((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \land (⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \leftrightarrow ((⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)))$
39	38	biimpac	$⊢ (((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \land (⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \land R = P) \to ((⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩))$
40		simpll	$⊢ ((⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to ⟨P, Q⟩ Cgr ⟨P, P⟩$
41		simp32	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to Q \in 𝔼 (N)$
42		axcgrid	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \in 𝔼 (N))) \to (⟨P, Q⟩ Cgr ⟨P, P⟩ \to P = Q)$
43	22 24 41 24 42	syl13anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨P, Q⟩ Cgr ⟨P, P⟩ \to P = Q)$
44	40 43	syl5	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to P = Q)$
45		simprlr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩))) \to ⟨C, P⟩ Cgr ⟨C, d⟩$
46		simpr3	$⊢ ((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩)) \to ⟨d, D⟩ Cgr ⟨P, P⟩$
47		simp2l2	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to D \in 𝔼 (N)$
48		axcgrid	$⊢ (N \in ℕ \land (d \in 𝔼 (N) \land D \in 𝔼 (N) \land P \in 𝔼 (N))) \to (⟨d, D⟩ Cgr ⟨P, P⟩ \to d = D)$
49	22 25 47 24 48	syl13anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨d, D⟩ Cgr ⟨P, P⟩ \to d = D)$
50	46 49	syl5	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩)) \to d = D)$
51	50	imp	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩))) \to d = D$
52	51	opeq2d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩))) \to ⟨C, d⟩ = ⟨C, D⟩$
53	52	breq2d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨C, P⟩ Cgr ⟨C, D⟩)$
54		simp2l1	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to C \in 𝔼 (N)$
55		cgrcomlr	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land P \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨C, P⟩ Cgr ⟨C, D⟩ \leftrightarrow ⟨P, C⟩ Cgr ⟨D, C⟩)$
56	22 54 24 54 47 55	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨C, P⟩ Cgr ⟨C, D⟩ \leftrightarrow ⟨P, C⟩ Cgr ⟨D, C⟩)$
57		cgrcom	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨P, C⟩ Cgr ⟨D, C⟩ \leftrightarrow ⟨D, C⟩ Cgr ⟨P, C⟩)$
58	22 24 54 47 54 57	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨P, C⟩ Cgr ⟨D, C⟩ \leftrightarrow ⟨D, C⟩ Cgr ⟨P, C⟩)$
59	56 58	bitrd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨C, P⟩ Cgr ⟨C, D⟩ \leftrightarrow ⟨D, C⟩ Cgr ⟨P, C⟩)$
60	59	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩))) \to (⟨C, P⟩ Cgr ⟨C, D⟩ \leftrightarrow ⟨D, C⟩ Cgr ⟨P, C⟩)$
61	53 60	bitrd	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨D, C⟩ Cgr ⟨P, C⟩)$
62	45 61	mpbid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩))) \to ⟨D, C⟩ Cgr ⟨P, C⟩$
63	62	ex	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩)) \to ⟨D, C⟩ Cgr ⟨P, C⟩)$
64		opeq2	$⊢ P = Q \to ⟨P, P⟩ = ⟨P, Q⟩$
65	64	breq1d	$⊢ P = Q \to (⟨P, P⟩ Cgr ⟨P, P⟩ \leftrightarrow ⟨P, Q⟩ Cgr ⟨P, P⟩)$
66	65	anbi1d	$⊢ P = Q \to ((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \leftrightarrow (⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩))$
67	64	breq1d	$⊢ P = Q \to (⟨P, P⟩ Cgr ⟨d, D⟩ \leftrightarrow ⟨P, Q⟩ Cgr ⟨d, D⟩)$
68	64	breq2d	$⊢ P = Q \to (⟨d, D⟩ Cgr ⟨P, P⟩ \leftrightarrow ⟨d, D⟩ Cgr ⟨P, Q⟩)$
69	67 68	3anbi23d	$⊢ P = Q \to ((⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩) \leftrightarrow (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩))$
70	66 69	anbi12d	$⊢ P = Q \to (((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩)) \leftrightarrow ((⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)))$
71		opeq1	$⊢ P = Q \to ⟨P, C⟩ = ⟨Q, C⟩$
72	71	breq2d	$⊢ P = Q \to (⟨D, C⟩ Cgr ⟨P, C⟩ \leftrightarrow ⟨D, C⟩ Cgr ⟨Q, C⟩)$
73	70 72	imbi12d	$⊢ P = Q \to ((((⟨P, P⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, P⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, P⟩)) \to ⟨D, C⟩ Cgr ⟨P, C⟩) \leftrightarrow (((⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to ⟨D, C⟩ Cgr ⟨Q, C⟩))$
74	63 73	syl5ibcom	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (P = Q \to (((⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to ⟨D, C⟩ Cgr ⟨Q, C⟩))$
75	74	com23	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to (P = Q \to ⟨D, C⟩ Cgr ⟨Q, C⟩))$
76	44 75	mpdd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((⟨P, Q⟩ Cgr ⟨P, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (⟨P, P⟩ Cgr ⟨d, d⟩ \land ⟨P, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)$
77	39 76	syl5	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to ((((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \land (⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \land R = P) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)$
78	77	expd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \land (⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to (R = P \to ⟨D, C⟩ Cgr ⟨Q, C⟩))$
79	28 78	mpdd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, d⟩) \land (⟨R, P⟩ Cgr ⟨d, d⟩ \land ⟨R, Q⟩ Cgr ⟨d, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩)) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)$
80	20 79	syl5	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to ((d = E \land ((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩))) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)$
81	80	exp4d	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (d = E \to ((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \to ((⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)))$
82	81	com23	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to ((⟨R, Q⟩ Cgr ⟨R, P⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \to (d = E \to ((⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)))$
83	10 82	syl5	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to (d = E \to ((⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)))$
84	83	imp31	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \land d = E) \to ((⟨R, P⟩ Cgr ⟨E, d⟩ \land ⟨R, Q⟩ Cgr ⟨E, D⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)$
85	5 84	mpd	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \land d = E) \to ⟨D, C⟩ Cgr ⟨Q, C⟩$
86		simp2r3	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to E \in 𝔼 (N)$
87		simprlr	$⊢ ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩)))) \to E Btwn ⟨D, d⟩$
88	87	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to E Btwn ⟨D, d⟩$
89	22 86 47 25 88	btwncomand	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to E Btwn ⟨d, D⟩$
90		cgrcomlr	$⊢ (N \in ℕ \land (R \in 𝔼 (N) \land P \in 𝔼 (N)) \land (E \in 𝔼 (N) \land d \in 𝔼 (N))) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \leftrightarrow ⟨P, R⟩ Cgr ⟨d, E⟩)$
91	22 23 24 86 25 90	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \leftrightarrow ⟨P, R⟩ Cgr ⟨d, E⟩)$
92		cgrcom	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land R \in 𝔼 (N)) \land (d \in 𝔼 (N) \land E \in 𝔼 (N))) \to (⟨P, R⟩ Cgr ⟨d, E⟩ \leftrightarrow ⟨d, E⟩ Cgr ⟨P, R⟩)$
93	22 24 23 25 86 92	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨P, R⟩ Cgr ⟨d, E⟩ \leftrightarrow ⟨d, E⟩ Cgr ⟨P, R⟩)$
94	91 93	bitrd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \leftrightarrow ⟨d, E⟩ Cgr ⟨P, R⟩)$
95	94	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨R, P⟩ Cgr ⟨E, d⟩ \leftrightarrow ⟨d, E⟩ Cgr ⟨P, R⟩)$
96	1 95	mpbid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, E⟩ Cgr ⟨P, R⟩$
97	22 23 41 86 47 2	cgrcomand	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨E, D⟩ Cgr ⟨R, Q⟩$
98		brcgr3	$⊢ (N \in ℕ \land (d \in 𝔼 (N) \land E \in 𝔼 (N) \land D \in 𝔼 (N)) \land (P \in 𝔼 (N) \land R \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \leftrightarrow (⟨d, E⟩ Cgr ⟨P, R⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩ \land ⟨E, D⟩ Cgr ⟨R, Q⟩))$
99	22 25 86 47 24 23 41 98	syl133anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \leftrightarrow (⟨d, E⟩ Cgr ⟨P, R⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩ \land ⟨E, D⟩ Cgr ⟨R, Q⟩))$
100	99	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \leftrightarrow (⟨d, E⟩ Cgr ⟨P, R⟩ \land ⟨d, D⟩ Cgr ⟨P, Q⟩ \land ⟨E, D⟩ Cgr ⟨R, Q⟩))$
101	96 3 97 100	mpbir3and	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩$
102		simpr1r	$⊢ ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))) \to ⟨C, P⟩ Cgr ⟨C, d⟩$
103	102	ad2antll	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨C, P⟩ Cgr ⟨C, d⟩$
104		cgrcomlr	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land P \in 𝔼 (N)) \land (C \in 𝔼 (N) \land d \in 𝔼 (N))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨P, C⟩ Cgr ⟨d, C⟩)$
105	22 54 24 54 25 104	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨P, C⟩ Cgr ⟨d, C⟩)$
106		cgrcom	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land C \in 𝔼 (N)) \land (d \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨P, C⟩ Cgr ⟨d, C⟩ \leftrightarrow ⟨d, C⟩ Cgr ⟨P, C⟩)$
107	22 24 54 25 54 106	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨P, C⟩ Cgr ⟨d, C⟩ \leftrightarrow ⟨d, C⟩ Cgr ⟨P, C⟩)$
108	105 107	bitrd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨d, C⟩ Cgr ⟨P, C⟩)$
109	108	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨C, P⟩ Cgr ⟨C, d⟩ \leftrightarrow ⟨d, C⟩ Cgr ⟨P, C⟩)$
110	103 109	mpbid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨d, C⟩ Cgr ⟨P, C⟩$
111	8	ad2antll	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨C, R⟩ Cgr ⟨C, E⟩$
112		cgrcomlr	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land R \in 𝔼 (N)) \land (C \in 𝔼 (N) \land E \in 𝔼 (N))) \to (⟨C, R⟩ Cgr ⟨C, E⟩ \leftrightarrow ⟨R, C⟩ Cgr ⟨E, C⟩)$
113	22 54 23 54 86 112	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨C, R⟩ Cgr ⟨C, E⟩ \leftrightarrow ⟨R, C⟩ Cgr ⟨E, C⟩)$
114		cgrcom	$⊢ (N \in ℕ \land (R \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨R, C⟩ Cgr ⟨E, C⟩ \leftrightarrow ⟨E, C⟩ Cgr ⟨R, C⟩)$
115	22 23 54 86 54 114	syl122anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨R, C⟩ Cgr ⟨E, C⟩ \leftrightarrow ⟨E, C⟩ Cgr ⟨R, C⟩)$
116	113 115	bitrd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (⟨C, R⟩ Cgr ⟨C, E⟩ \leftrightarrow ⟨E, C⟩ Cgr ⟨R, C⟩)$
117	116	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨C, R⟩ Cgr ⟨C, E⟩ \leftrightarrow ⟨E, C⟩ Cgr ⟨R, C⟩)$
118	111 117	mpbid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨E, C⟩ Cgr ⟨R, C⟩$
119	110 118	jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨E, C⟩ Cgr ⟨R, C⟩)$
120	89 101 119	3jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to (E Btwn ⟨d, D⟩ \land ⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \land (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨E, C⟩ Cgr ⟨R, C⟩))$
121	120	adantr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \land d \neq E) \to (E Btwn ⟨d, D⟩ \land ⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \land (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨E, C⟩ Cgr ⟨R, C⟩))$
122		simpr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \land d \neq E) \to d \neq E$
123		brofs2	$⊢ ((N \in ℕ \land d \in 𝔼 (N) \land E \in 𝔼 (N)) \land (D \in 𝔼 (N) \land C \in 𝔼 (N) \land P \in 𝔼 (N)) \land (R \in 𝔼 (N) \land Q \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨⟨d, E⟩, ⟨D, C⟩⟩ OuterFiveSeg ⟨⟨P, R⟩, ⟨Q, C⟩⟩ \leftrightarrow (E Btwn ⟨d, D⟩ \land ⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \land (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨E, C⟩ Cgr ⟨R, C⟩)))$
124	123	anbi1d	$⊢ ((N \in ℕ \land d \in 𝔼 (N) \land E \in 𝔼 (N)) \land (D \in 𝔼 (N) \land C \in 𝔼 (N) \land P \in 𝔼 (N)) \land (R \in 𝔼 (N) \land Q \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((⟨⟨d, E⟩, ⟨D, C⟩⟩ OuterFiveSeg ⟨⟨P, R⟩, ⟨Q, C⟩⟩ \land d \neq E) \leftrightarrow ((E Btwn ⟨d, D⟩ \land ⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \land (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨E, C⟩ Cgr ⟨R, C⟩)) \land d \neq E))$
125		5segofs	$⊢ ((N \in ℕ \land d \in 𝔼 (N) \land E \in 𝔼 (N)) \land (D \in 𝔼 (N) \land C \in 𝔼 (N) \land P \in 𝔼 (N)) \land (R \in 𝔼 (N) \land Q \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((⟨⟨d, E⟩, ⟨D, C⟩⟩ OuterFiveSeg ⟨⟨P, R⟩, ⟨Q, C⟩⟩ \land d \neq E) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)$
126	124 125	sylbird	$⊢ ((N \in ℕ \land d \in 𝔼 (N) \land E \in 𝔼 (N)) \land (D \in 𝔼 (N) \land C \in 𝔼 (N) \land P \in 𝔼 (N)) \land (R \in 𝔼 (N) \land Q \in 𝔼 (N) \land C \in 𝔼 (N))) \to (((E Btwn ⟨d, D⟩ \land ⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \land (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨E, C⟩ Cgr ⟨R, C⟩)) \land d \neq E) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)$
127	22 25 86 47 54 24 23 41 54 126	syl333anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \to (((E Btwn ⟨d, D⟩ \land ⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \land (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨E, C⟩ Cgr ⟨R, C⟩)) \land d \neq E) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)$
128	127	ad2antrr	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \land d \neq E) \to (((E Btwn ⟨d, D⟩ \land ⟨d, ⟨E, D⟩⟩ Cgr3 ⟨P, ⟨R, Q⟩⟩ \land (⟨d, C⟩ Cgr ⟨P, C⟩ \land ⟨E, C⟩ Cgr ⟨R, C⟩)) \land d \neq E) \to ⟨D, C⟩ Cgr ⟨Q, C⟩)$
129	121 122 128	mp2and	$⊢ ((((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \land d \neq E) \to ⟨D, C⟩ Cgr ⟨Q, C⟩$
130	85 129	pm2.61dane	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land ((C \in 𝔼 (N) \land D \in 𝔼 (N) \land c \in 𝔼 (N)) \land (d \in 𝔼 (N) \land b \in 𝔼 (N) \land E \in 𝔼 (N))) \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land R \in 𝔼 (N))) \land ((((A \neq B \land B \neq C \land C \neq c) \land (B Btwn ⟨A, C⟩ \land B Btwn ⟨A, D⟩)) \land ((D Btwn ⟨A, c⟩ \land ⟨D, c⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨A, d⟩ \land ⟨C, d⟩ Cgr ⟨C, D⟩)) \land ((c Btwn ⟨A, b⟩ \land ⟨c, b⟩ Cgr ⟨C, B⟩) \land (d Btwn ⟨A, b⟩ \land ⟨d, b⟩ Cgr ⟨D, B⟩))) \land ((E Btwn ⟨C, c⟩ \land E Btwn ⟨D, d⟩) \land ((C Btwn ⟨c, P⟩ \land ⟨C, P⟩ Cgr ⟨C, d⟩) \land (C Btwn ⟨d, R⟩ \land ⟨C, R⟩ Cgr ⟨C, E⟩) \land (R Btwn ⟨P, Q⟩ \land ⟨R, Q⟩ Cgr ⟨R, P⟩))))) \to ⟨D, C⟩ Cgr ⟨Q, C⟩$

Metamath Proof Explorer

Theorem btwnconn1lem11

Proof