dfcgra2

Description: This is the full statement of definition 11.2 of Schwabhauser p. 95. This proof serves to confirm that the definition we have chosen, df-cgra is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020)

	Ref	Expression
Hypotheses	dfcgra2.p	$⊢ P = {Base}_{G}$
	dfcgra2.i	$⊢ I = Itv (G)$
	dfcgra2.m	$⊢ \underset{˙}{-} = dist (G)$
	dfcgra2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	dfcgra2.a	$⊢ φ \to A \in P$
	dfcgra2.b	$⊢ φ \to B \in P$
	dfcgra2.c	$⊢ φ \to C \in P$
	dfcgra2.d	$⊢ φ \to D \in P$
	dfcgra2.e	$⊢ φ \to E \in P$
	dfcgra2.f	$⊢ φ \to F \in P$
Assertion	dfcgra2	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)))$

Proof

Step	Hyp	Ref	Expression
1		dfcgra2.p	$⊢ P = {Base}_{G}$
2		dfcgra2.i	$⊢ I = Itv (G)$
3		dfcgra2.m	$⊢ \underset{˙}{-} = dist (G)$
4		dfcgra2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		dfcgra2.a	$⊢ φ \to A \in P$
6		dfcgra2.b	$⊢ φ \to B \in P$
7		dfcgra2.c	$⊢ φ \to C \in P$
8		dfcgra2.d	$⊢ φ \to D \in P$
9		dfcgra2.e	$⊢ φ \to E \in P$
10		dfcgra2.f	$⊢ φ \to F \in P$
11		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
12	4	adantr	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to G \in 𝒢_{Tarski}$
13	5	adantr	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to A \in P$
14	6	adantr	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to B \in P$
15	7	adantr	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to C \in P$
16	8	adantr	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to D \in P$
17	9	adantr	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to E \in P$
18	10	adantr	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to F \in P$
19		simpr	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
20	1 2 11 12 13 14 15 16 17 18 19	cgrane1	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to A \neq B$
21	1 2 11 12 13 14 15 16 17 18 19	cgrane2	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to B \neq C$
22	21	necomd	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to C \neq B$
23	20 22	jca	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to (A \neq B \land C \neq B)$
24	1 2 11 12 13 14 15 16 17 18 19	cgrane3	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to E \neq D$
25	24	necomd	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to D \neq E$
26	1 2 11 12 13 14 15 16 17 18 19	cgrane4	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to E \neq F$
27	26	necomd	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to F \neq E$
28	25 27	jca	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to (D \neq E \land F \neq E)$
29		simprl	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F))$
30		simprr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))$
31	4	ad6antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to G \in 𝒢_{Tarski}$
32		simp-5r	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to a \in P$
33	6	ad6antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to B \in P$
34		simp-4r	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to c \in P$
35		simpllr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to d \in P$
36	9	ad6antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to E \in P$
37		simplr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to f \in P$
38	10	ad6antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to F \in P$
39	8	ad6antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to D \in P$
40	7	ad6antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to C \in P$
41	5	ad6antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to A \in P$
42		simp-6r	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
43	1 2 31 11 41 33 40 39 36 38 42	cgracom	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
44	29	simplld	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to A \in (B I a)$
45	20	ad5antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to A \neq B$
46	1 3 2 31 33 41 32 44 45	tgbtwnne	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to B \neq a$
47	1 2 11 33 32 41 31 41 44 46 45	btwnhl1	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to A {hl}_{𝒢} (G) (B) a$
48	1 2 11 41 32 33 31 47	hlcomd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to a {hl}_{𝒢} (G) (B) A$
49	1 2 11 31 39 36 38 41 33 40 43 32 48	cgrahl1	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ a B C ”⟩$
50	29	simprld	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to C \in (B I c)$
51	22	ad5antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to C \neq B$
52	1 3 2 31 33 40 34 50 51	tgbtwnne	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to B \neq c$
53	1 2 11 33 34 40 31 41 50 52 51	btwnhl1	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to C {hl}_{𝒢} (G) (B) c$
54	1 2 11 40 34 33 31 53	hlcomd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to c {hl}_{𝒢} (G) (B) C$
55	1 2 11 31 39 36 38 32 33 40 49 34 54	cgrahl2	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ a B c ”⟩$
56	1 2 31 11 39 36 38 32 33 34 55	cgracom	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to ⟨“ a B c ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
57	30	simplld	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to D \in (E I d)$
58	25	ad5antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to D \neq E$
59	1 3 2 31 36 39 35 57 58	tgbtwnne	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to E \neq d$
60	1 2 11 36 35 39 31 41 57 59 58	btwnhl1	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to D {hl}_{𝒢} (G) (E) d$
61	1 2 11 39 35 36 31 60	hlcomd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to d {hl}_{𝒢} (G) (E) D$
62	1 2 11 31 32 33 34 39 36 38 56 35 61	cgrahl1	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to ⟨“ a B c ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ d E F ”⟩$
63	30	simprld	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to F \in (E I f)$
64	27	ad5antr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to F \neq E$
65	1 3 2 31 36 38 37 63 64	tgbtwnne	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to E \neq f$
66	1 2 11 36 37 38 31 41 63 65 64	btwnhl1	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to F {hl}_{𝒢} (G) (E) f$
67	1 2 11 38 37 36 31 66	hlcomd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to f {hl}_{𝒢} (G) (E) F$
68	1 2 11 31 32 33 34 35 36 38 62 37 67	cgrahl2	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to ⟨“ a B c ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ d E f ”⟩$
69	46	necomd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to a \neq B$
70	1 2 11 32 41 33 31 69	hlid	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to a {hl}_{𝒢} (G) (B) a$
71	52	necomd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to c \neq B$
72	1 2 11 34 41 33 31 71	hlid	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to c {hl}_{𝒢} (G) (B) c$
73	1 3 2 31 33 41 32 44	tgbtwncom	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to A \in (a I B)$
74	29	simplrd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to A \underset{˙}{-} a = E \underset{˙}{-} D$
75	1 3 2 31 41 32 36 39 74	tgcgrcoml	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to a \underset{˙}{-} A = E \underset{˙}{-} D$
76	30	simplrd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to D \underset{˙}{-} d = B \underset{˙}{-} A$
77	76	eqcomd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to B \underset{˙}{-} A = D \underset{˙}{-} d$
78	1 3 2 31 33 41 39 35 77	tgcgrcoml	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to A \underset{˙}{-} B = D \underset{˙}{-} d$
79	1 3 2 31 32 41 33 36 39 35 73 57 75 78	tgcgrextend	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to a \underset{˙}{-} B = E \underset{˙}{-} d$
80	1 3 2 31 32 33 36 35 79	tgcgrcoml	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to B \underset{˙}{-} a = E \underset{˙}{-} d$
81	1 3 2 31 33 40 34 50	tgbtwncom	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to C \in (c I B)$
82	29	simprrd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to C \underset{˙}{-} c = E \underset{˙}{-} F$
83	1 3 2 31 40 34 36 38 82	tgcgrcoml	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to c \underset{˙}{-} C = E \underset{˙}{-} F$
84	30	simprrd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to F \underset{˙}{-} f = B \underset{˙}{-} C$
85	84	eqcomd	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to B \underset{˙}{-} C = F \underset{˙}{-} f$
86	1 3 2 31 33 40 38 37 85	tgcgrcoml	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to C \underset{˙}{-} B = F \underset{˙}{-} f$
87	1 3 2 31 34 40 33 36 38 37 81 63 83 86	tgcgrextend	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to c \underset{˙}{-} B = E \underset{˙}{-} f$
88	1 3 2 31 34 33 36 37 87	tgcgrcoml	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to B \underset{˙}{-} c = E \underset{˙}{-} f$
89	1 2 11 31 32 33 34 35 36 37 68 32 3 34 70 72 80 88	cgracgr	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to a \underset{˙}{-} c = d \underset{˙}{-} f$
90	29 30 89	3jca	$⊢ ((((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \land (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)$
91	90	ex	$⊢ (((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \land f \in P) \to ((((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))) \to (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f))$
92	91	reximdva	$⊢ ((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land d \in P) \to (\exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))) \to \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f))$
93	92	reximdva	$⊢ (((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \to (\exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))) \to \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f))$
94	93	imp	$⊢ ((((φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \land a \in P) \land c \in P) \land \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))) \to \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)$
95	1 3 2 4 6 5 9 8	axtgsegcon	$⊢ φ \to \exists a \in P (A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D)$
96	1 3 2 4 6 7 9 10	axtgsegcon	$⊢ φ \to \exists c \in P (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)$
97		reeanv	$⊢ \exists a \in P \exists c \in P ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \leftrightarrow (\exists a \in P (A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land \exists c \in P (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F))$
98	95 96 97	sylanbrc	$⊢ φ \to \exists a \in P \exists c \in P ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F))$
99	1 3 2 4 9 8 6 5	axtgsegcon	$⊢ φ \to \exists d \in P (D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A)$
100	1 3 2 4 9 10 6 7	axtgsegcon	$⊢ φ \to \exists f \in P (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)$
101		reeanv	$⊢ \exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \leftrightarrow (\exists d \in P (D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land \exists f \in P (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))$
102	99 100 101	sylanbrc	$⊢ φ \to \exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))$
103	98 102	jca	$⊢ φ \to (\exists a \in P \exists c \in P ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land \exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
104		r19.41vv	$⊢ \exists d \in P \exists f \in P (((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F))) \leftrightarrow (\exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)))$
105		ancom	$⊢ (((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F))) \leftrightarrow (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
106	105	2rexbii	$⊢ \exists d \in P \exists f \in P (((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F))) \leftrightarrow \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
107		ancom	$⊢ (\exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F))) \leftrightarrow (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land \exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
108	104 106 107	3bitr3i	$⊢ \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))) \leftrightarrow (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land \exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
109	108	2rexbii	$⊢ \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))) \leftrightarrow \exists a \in P \exists c \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land \exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
110		r19.41vv	$⊢ \exists a \in P \exists c \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land \exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))) \leftrightarrow (\exists a \in P \exists c \in P ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land \exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
111	109 110	bitr2i	$⊢ (\exists a \in P \exists c \in P ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land \exists d \in P \exists f \in P ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C))) \leftrightarrow \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
112	103 111	sylib	$⊢ φ \to \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
113	112	adantr	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
114	94 113	reximddv2	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)$
115	23 28 114	3jca	$⊢ (φ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩) \to ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f))$
116		df-3an	$⊢ ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)) \leftrightarrow (((A \neq B \land C \neq B) \land (D \neq E \land F \neq E)) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f))$
117	4	ad6antr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to G \in 𝒢_{Tarski}$
118	8	ad6antr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to D \in P$
119	9	ad6antr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to E \in P$
120	10	ad6antr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to F \in P$
121	5	ad6antr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to A \in P$
122	6	ad6antr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to B \in P$
123	7	ad6antr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to C \in P$
124		simp-4r	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to y \in P$
125		simp-5r	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to x \in P$
126		simpllr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to z \in P$
127		simplr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to t \in P$
128		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
129		simpr1	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F))$
130	129	simplld	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to A \in (B I x)$
131		simpr2	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C))$
132	131	simplld	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to D \in (E I z)$
133	1 3 2 117 119 118 126 132	tgbtwncom	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to D \in (z I E)$
134	131	simplrd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to D \underset{˙}{-} z = B \underset{˙}{-} A$
135	134	eqcomd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to B \underset{˙}{-} A = D \underset{˙}{-} z$
136	1 3 2 117 122 121 118 126 135	tgcgrcomr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to B \underset{˙}{-} A = z \underset{˙}{-} D$
137	129	simplrd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to A \underset{˙}{-} x = E \underset{˙}{-} D$
138	1 3 2 117 121 125 119 118 137	tgcgrcomr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to A \underset{˙}{-} x = D \underset{˙}{-} E$
139	1 3 2 117 122 121 125 126 118 119 130 133 136 138	tgcgrextend	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to B \underset{˙}{-} x = z \underset{˙}{-} E$
140	1 3 2 117 122 125 126 119 139	tgcgrcoml	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to x \underset{˙}{-} B = z \underset{˙}{-} E$
141	129	simprld	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to C \in (B I y)$
142	1 3 2 117 122 123 124 141	tgbtwncom	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to C \in (y I B)$
143	131	simprld	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to F \in (E I t)$
144	129	simprrd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to C \underset{˙}{-} y = E \underset{˙}{-} F$
145	1 3 2 117 123 124 119 120 144	tgcgrcoml	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to y \underset{˙}{-} C = E \underset{˙}{-} F$
146	131	simprrd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to F \underset{˙}{-} t = B \underset{˙}{-} C$
147	146	eqcomd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to B \underset{˙}{-} C = F \underset{˙}{-} t$
148	1 3 2 117 122 123 120 127 147	tgcgrcoml	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to C \underset{˙}{-} B = F \underset{˙}{-} t$
149	1 3 2 117 124 123 122 119 120 127 142 143 145 148	tgcgrextend	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to y \underset{˙}{-} B = E \underset{˙}{-} t$
150	1 3 2 117 124 122 119 127 149	tgcgrcoml	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to B \underset{˙}{-} y = E \underset{˙}{-} t$
151		simpr3	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to x \underset{˙}{-} y = z \underset{˙}{-} t$
152	1 3 2 117 125 124 126 127 151	tgcgrcomlr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to y \underset{˙}{-} x = t \underset{˙}{-} z$
153	1 3 128 117 125 122 124 126 119 127 140 150 152	trgcgr	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ⟨“ x B y ”⟩ \sim_{𝒢} (G) ⟨“ z E t ”⟩$
154		simp-6r	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))$
155	154	simprld	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to D \neq E$
156	1 3 2 117 119 118 126 132 155	tgbtwnne	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to E \neq z$
157	1 2 11 119 126 118 117 122 132 156 155	btwnhl1	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to D {hl}_{𝒢} (G) (E) z$
158	1 2 11 118 126 119 117 157	hlcomd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to z {hl}_{𝒢} (G) (E) D$
159	154	simprrd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to F \neq E$
160	1 3 2 117 119 120 127 143 159	tgbtwnne	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to E \neq t$
161	1 2 11 119 127 120 117 122 143 160 159	btwnhl1	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to F {hl}_{𝒢} (G) (E) t$
162	1 2 11 120 127 119 117 161	hlcomd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to t {hl}_{𝒢} (G) (E) F$
163	1 2 11 117 125 122 124 118 119 120 126 127 153 158 162	iscgrad	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ⟨“ x B y ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
164	1 2 117 11 125 122 124 118 119 120 163	cgracom	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ x B y ”⟩$
165	154	simplld	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to A \neq B$
166	1 3 2 117 122 121 125 130 165	tgbtwnne	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to B \neq x$
167	1 2 11 122 125 121 117 121 130 166 165	btwnhl1	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to A {hl}_{𝒢} (G) (B) x$
168	1 2 11 117 118 119 120 125 122 124 164 121 167	cgrahl1	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B y ”⟩$
169	154	simplrd	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to C \neq B$
170	1 3 2 117 122 123 124 141 169	tgbtwnne	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to B \neq y$
171	1 2 11 122 124 123 117 121 141 170 169	btwnhl1	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to C {hl}_{𝒢} (G) (B) y$
172	1 2 11 117 118 119 120 121 122 124 168 123 171	cgrahl2	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
173	1 2 117 11 118 119 120 121 122 123 172	cgracom	$⊢ ((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
174	173	adantl3r	$⊢ (((((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f)) \land z \in P) \land t \in P) \land (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
175		simpr	$⊢ ((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f)) \to \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f)$
176		oveq2	$⊢ d = z \to E I d = E I z$
177	176	eleq2d	$⊢ d = z \to (D \in (E I d) \leftrightarrow D \in (E I z))$
178		oveq2	$⊢ d = z \to D \underset{˙}{-} d = D \underset{˙}{-} z$
179	178	eqeq1d	$⊢ d = z \to (D \underset{˙}{-} d = B \underset{˙}{-} A \leftrightarrow D \underset{˙}{-} z = B \underset{˙}{-} A)$
180	177 179	anbi12d	$⊢ d = z \to ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \leftrightarrow (D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A))$
181	180	anbi1d	$⊢ d = z \to (((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \leftrightarrow ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)))$
182		oveq1	$⊢ d = z \to d \underset{˙}{-} f = z \underset{˙}{-} f$
183	182	eqeq2d	$⊢ d = z \to (x \underset{˙}{-} y = d \underset{˙}{-} f \leftrightarrow x \underset{˙}{-} y = z \underset{˙}{-} f)$
184	181 183	3anbi23d	$⊢ d = z \to ((((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f) \leftrightarrow (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} f))$
185		oveq2	$⊢ f = t \to E I f = E I t$
186	185	eleq2d	$⊢ f = t \to (F \in (E I f) \leftrightarrow F \in (E I t))$
187		oveq2	$⊢ f = t \to F \underset{˙}{-} f = F \underset{˙}{-} t$
188	187	eqeq1d	$⊢ f = t \to (F \underset{˙}{-} f = B \underset{˙}{-} C \leftrightarrow F \underset{˙}{-} t = B \underset{˙}{-} C)$
189	186 188	anbi12d	$⊢ f = t \to ((F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C) \leftrightarrow (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C))$
190	189	anbi2d	$⊢ f = t \to (((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \leftrightarrow ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)))$
191		oveq2	$⊢ f = t \to z \underset{˙}{-} f = z \underset{˙}{-} t$
192	191	eqeq2d	$⊢ f = t \to (x \underset{˙}{-} y = z \underset{˙}{-} f \leftrightarrow x \underset{˙}{-} y = z \underset{˙}{-} t)$
193	190 192	3anbi23d	$⊢ f = t \to ((((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} f) \leftrightarrow (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t))$
194	184 193	cbvrex2vw	$⊢ \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f) \leftrightarrow \exists z \in P \exists t \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)$
195	175 194	sylib	$⊢ ((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f)) \to \exists z \in P \exists t \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I z) \land D \underset{˙}{-} z = B \underset{˙}{-} A) \land (F \in (E I t) \land F \underset{˙}{-} t = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = z \underset{˙}{-} t)$
196	174 195	r19.29vva	$⊢ ((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land x \in P) \land y \in P) \land \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
197	196	adantl3r	$⊢ (((((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)) \land x \in P) \land y \in P) \land \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
198		simpr	$⊢ ((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)) \to \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)$
199		oveq2	$⊢ a = x \to B I a = B I x$
200	199	eleq2d	$⊢ a = x \to (A \in (B I a) \leftrightarrow A \in (B I x))$
201		oveq2	$⊢ a = x \to A \underset{˙}{-} a = A \underset{˙}{-} x$
202	201	eqeq1d	$⊢ a = x \to (A \underset{˙}{-} a = E \underset{˙}{-} D \leftrightarrow A \underset{˙}{-} x = E \underset{˙}{-} D)$
203	200 202	anbi12d	$⊢ a = x \to ((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \leftrightarrow (A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D))$
204	203	anbi1d	$⊢ a = x \to (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \leftrightarrow ((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)))$
205		oveq1	$⊢ a = x \to a \underset{˙}{-} c = x \underset{˙}{-} c$
206	205	eqeq1d	$⊢ a = x \to (a \underset{˙}{-} c = d \underset{˙}{-} f \leftrightarrow x \underset{˙}{-} c = d \underset{˙}{-} f)$
207	204 206	3anbi13d	$⊢ a = x \to ((((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f) \leftrightarrow (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} c = d \underset{˙}{-} f))$
208	207	2rexbidv	$⊢ a = x \to (\exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f) \leftrightarrow \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} c = d \underset{˙}{-} f))$
209		oveq2	$⊢ c = y \to B I c = B I y$
210	209	eleq2d	$⊢ c = y \to (C \in (B I c) \leftrightarrow C \in (B I y))$
211		oveq2	$⊢ c = y \to C \underset{˙}{-} c = C \underset{˙}{-} y$
212	211	eqeq1d	$⊢ c = y \to (C \underset{˙}{-} c = E \underset{˙}{-} F \leftrightarrow C \underset{˙}{-} y = E \underset{˙}{-} F)$
213	210 212	anbi12d	$⊢ c = y \to ((C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F) \leftrightarrow (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F))$
214	213	anbi2d	$⊢ c = y \to (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \leftrightarrow ((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)))$
215		oveq2	$⊢ c = y \to x \underset{˙}{-} c = x \underset{˙}{-} y$
216	215	eqeq1d	$⊢ c = y \to (x \underset{˙}{-} c = d \underset{˙}{-} f \leftrightarrow x \underset{˙}{-} y = d \underset{˙}{-} f)$
217	214 216	3anbi13d	$⊢ c = y \to ((((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} c = d \underset{˙}{-} f) \leftrightarrow (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f))$
218	217	2rexbidv	$⊢ c = y \to (\exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} c = d \underset{˙}{-} f) \leftrightarrow \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f))$
219	208 218	cbvrex2vw	$⊢ \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f) \leftrightarrow \exists x \in P \exists y \in P \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f)$
220	198 219	sylib	$⊢ ((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)) \to \exists x \in P \exists y \in P \exists d \in P \exists f \in P (((A \in (B I x) \land A \underset{˙}{-} x = E \underset{˙}{-} D) \land (C \in (B I y) \land C \underset{˙}{-} y = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land x \underset{˙}{-} y = d \underset{˙}{-} f)$
221	197 220	r19.29vva	$⊢ ((φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E))) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
222	221	anasss	$⊢ (φ \land (((A \neq B \land C \neq B) \land (D \neq E \land F \neq E)) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f))) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
223	116 222	sylan2b	$⊢ (φ \land ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f))) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
224	115 223	impbida	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow ((A \neq B \land C \neq B) \land (D \neq E \land F \neq E) \land \exists a \in P \exists c \in P \exists d \in P \exists f \in P (((A \in (B I a) \land A \underset{˙}{-} a = E \underset{˙}{-} D) \land (C \in (B I c) \land C \underset{˙}{-} c = E \underset{˙}{-} F)) \land ((D \in (E I d) \land D \underset{˙}{-} d = B \underset{˙}{-} A) \land (F \in (E I f) \land F \underset{˙}{-} f = B \underset{˙}{-} C)) \land a \underset{˙}{-} c = d \underset{˙}{-} f)))$

Metamath Proof Explorer

Theorem dfcgra2

Proof