tgasa1

Description: Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of Schwabhauser p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020)

	Ref	Expression
Hypotheses	tgsas.p	$⊢ P = {Base}_{G}$
	tgsas.m	$⊢ \underset{˙}{-} = dist (G)$
	tgsas.i	$⊢ I = Itv (G)$
	tgsas.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgsas.a	$⊢ φ \to A \in P$
	tgsas.b	$⊢ φ \to B \in P$
	tgsas.c	$⊢ φ \to C \in P$
	tgsas.d	$⊢ φ \to D \in P$
	tgsas.e	$⊢ φ \to E \in P$
	tgsas.f	$⊢ φ \to F \in P$
	tgasa.l	$⊢ L = {Line}_{𝒢} (G)$
	tgasa.1	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
	tgasa.2	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
	tgasa.3	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	tgasa.4	$⊢ φ \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ F D E ”⟩$
Assertion	tgasa1	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} F$

Proof

Step	Hyp	Ref	Expression
1		tgsas.p	$⊢ P = {Base}_{G}$
2		tgsas.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgsas.i	$⊢ I = Itv (G)$
4		tgsas.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tgsas.a	$⊢ φ \to A \in P$
6		tgsas.b	$⊢ φ \to B \in P$
7		tgsas.c	$⊢ φ \to C \in P$
8		tgsas.d	$⊢ φ \to D \in P$
9		tgsas.e	$⊢ φ \to E \in P$
10		tgsas.f	$⊢ φ \to F \in P$
11		tgasa.l	$⊢ L = {Line}_{𝒢} (G)$
12		tgasa.1	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
13		tgasa.2	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
14		tgasa.3	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
15		tgasa.4	$⊢ φ \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ F D E ”⟩$
16		simprr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to E \underset{˙}{-} f = B \underset{˙}{-} C$
17	4	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to G \in 𝒢_{Tarski}$
18	10	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to F \in P$
19	8	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \in P$
20	9	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to E \in P$
21	1 3 2 4 5 6 7 8 9 10 14 11 12	cgrancol	$⊢ φ \to \neg (F \in (D L E) \lor D = E)$
22	21	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to \neg (F \in (D L E) \lor D = E)$
23		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
24		simplr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f \in P$
25	7	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to C \in P$
26	5	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to A \in P$
27	6	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to B \in P$
28	12	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to \neg (C \in (A L B) \lor A = B)$
29	4	ad3antrrr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to G \in 𝒢_{Tarski}$
30	8	ad3antrrr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to D \in P$
31	9	ad3antrrr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to E \in P$
32	10	ad3antrrr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to F \in P$
33	5	ad3antrrr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to A \in P$
34	6	ad3antrrr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to B \in P$
35	7	ad3antrrr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to C \in P$
36	1 3 4 23 5 6 7 8 9 10 14	cgracom	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
37	36	ad3antrrr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
38		simpr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to (E \in (D L F) \lor D = F)$
39	1 11 3 29 30 32 31 38	colcom	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to (E \in (F L D) \lor F = D)$
40	1 11 3 29 32 30 31 39	colrot1	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to (F \in (D L E) \lor D = E)$
41	1 3 2 29 30 31 32 33 34 35 37 11 40	cgracol	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to (C \in (A L B) \lor A = B)$
42	12	ad3antrrr	$⊢ (((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \land (E \in (D L F) \lor D = F)) \to \neg (C \in (A L B) \lor A = B)$
43	41 42	pm2.65da	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to \neg (E \in (D L F) \lor D = F)$
44		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
45	14	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
46		simprl	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f {hl}_{𝒢} (G) (E) F$
47	1 3 23 17 26 27 25 19 20 18 45 24 46	cgrahl2	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E f ”⟩$
48	1 3 23 4 5 6 7 8 9 10 14	cgrane1	$⊢ φ \to A \neq B$
49	1 3 23 5 5 6 4 48	hlid	$⊢ φ \to A {hl}_{𝒢} (G) (B) A$
50	49	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to A {hl}_{𝒢} (G) (B) A$
51	1 3 23 4 5 6 7 8 9 10 14	cgrane2	$⊢ φ \to B \neq C$
52	51	necomd	$⊢ φ \to C \neq B$
53	1 3 23 7 5 6 4 52	hlid	$⊢ φ \to C {hl}_{𝒢} (G) (B) C$
54	53	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to C {hl}_{𝒢} (G) (B) C$
55	1 2 3 4 5 6 8 9 13	tgcgrcomlr	$⊢ φ \to B \underset{˙}{-} A = E \underset{˙}{-} D$
56	55	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to B \underset{˙}{-} A = E \underset{˙}{-} D$
57	16	eqcomd	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to B \underset{˙}{-} C = E \underset{˙}{-} f$
58	1 3 23 17 26 27 25 19 20 24 47 26 2 25 50 54 56 57	cgracgr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to A \underset{˙}{-} C = D \underset{˙}{-} f$
59	1 2 3 17 26 25 19 24 58	tgcgrcomlr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to C \underset{˙}{-} A = f \underset{˙}{-} D$
60	13	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
61	1 2 44 17 25 26 27 24 19 20 59 60 57	trgcgr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to ⟨“ C A B ”⟩ \sim_{𝒢} (G) ⟨“ f D E ”⟩$
62	1 3 11 4 7 5 6 12	ncolne1	$⊢ φ \to C \neq A$
63	62	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to C \neq A$
64	1 2 3 17 25 26 24 19 59 63	tgcgrneq	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f \neq D$
65	1 3 23 24 18 19 17 64	hlid	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f {hl}_{𝒢} (G) (D) f$
66	1 3 23 4 7 5 6 10 8 9 15	cgrane4	$⊢ φ \to D \neq E$
67	66	necomd	$⊢ φ \to E \neq D$
68	1 3 23 9 5 8 4 67	hlid	$⊢ φ \to E {hl}_{𝒢} (G) (D) E$
69	68	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to E {hl}_{𝒢} (G) (D) E$
70	1 3 23 17 25 26 27 24 19 20 24 20 61 65 69	iscgrad	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ f D E ”⟩$
71	66	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to D \neq E$
72	1 3 17 23 24 19 20 64 71	cgraswap	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to ⟨“ f D E ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ E D f ”⟩$
73	1 3 17 23 25 26 27 24 19 20 70 20 19 24 72	cgratr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ E D f ”⟩$
74	1 3 23 4 7 5 6 10 8 9 15	cgrane3	$⊢ φ \to D \neq F$
75	74	necomd	$⊢ φ \to F \neq D$
76	1 3 4 23 10 8 9 75 66	cgraswap	$⊢ φ \to ⟨“ F D E ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ E D F ”⟩$
77	1 3 4 23 7 5 6 10 8 9 15 9 8 10 76	cgratr	$⊢ φ \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ E D F ”⟩$
78	77	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ E D F ”⟩$
79	1 3 11 4 9 8 67	tgelrnln	$⊢ φ \to E L D \in ran L$
80	79	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to E L D \in ran L$
81		simpl	$⊢ (a = u \land b = v) \to a = u$
82	81	eleq1d	$⊢ (a = u \land b = v) \to (a \in (P ∖ (E L D)) \leftrightarrow u \in (P ∖ (E L D)))$
83		simpr	$⊢ (a = u \land b = v) \to b = v$
84	83	eleq1d	$⊢ (a = u \land b = v) \to (b \in (P ∖ (E L D)) \leftrightarrow v \in (P ∖ (E L D)))$
85	82 84	anbi12d	$⊢ (a = u \land b = v) \to ((a \in (P ∖ (E L D)) \land b \in (P ∖ (E L D))) \leftrightarrow (u \in (P ∖ (E L D)) \land v \in (P ∖ (E L D))))$
86		simpr	$⊢ ((a = u \land b = v) \land t = w) \to t = w$
87		simpll	$⊢ ((a = u \land b = v) \land t = w) \to a = u$
88		simplr	$⊢ ((a = u \land b = v) \land t = w) \to b = v$
89	87 88	oveq12d	$⊢ ((a = u \land b = v) \land t = w) \to a I b = u I v$
90	86 89	eleq12d	$⊢ ((a = u \land b = v) \land t = w) \to (t \in (a I b) \leftrightarrow w \in (u I v))$
91	90	cbvrexdva	$⊢ (a = u \land b = v) \to (\exists t \in (E L D) t \in (a I b) \leftrightarrow \exists w \in (E L D) w \in (u I v))$
92	85 91	anbi12d	$⊢ (a = u \land b = v) \to (((a \in (P ∖ (E L D)) \land b \in (P ∖ (E L D))) \land \exists t \in (E L D) t \in (a I b)) \leftrightarrow ((u \in (P ∖ (E L D)) \land v \in (P ∖ (E L D))) \land \exists w \in (E L D) w \in (u I v)))$
93	92	cbvopabv	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ (E L D)) \land b \in (P ∖ (E L D))) \land \exists t \in (E L D) t \in (a I b))\} = \{⟨u, v⟩ \| ((u \in (P ∖ (E L D)) \land v \in (P ∖ (E L D))) \land \exists w \in (E L D) w \in (u I v))\}$
94	1 3 11 4 9 8 67	tglinerflx1	$⊢ φ \to E \in (E L D)$
95	94	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to E \in (E L D)$
96	1 11 3 4 8 9 10 21	ncolcom	$⊢ φ \to \neg (F \in (E L D) \lor E = D)$
97		pm2.45	$⊢ \neg (F \in (E L D) \lor E = D) \to \neg F \in (E L D)$
98	96 97	syl	$⊢ φ \to \neg F \in (E L D)$
99	98	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to \neg F \in (E L D)$
100	1 3 23 24 18 20 17 46	hlcomd	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to F {hl}_{𝒢} (G) (E) f$
101	1 3 11 17 80 20 93 23 95 18 24 99 100	hphl	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to F {hp}_{𝒢} (G) (E L D) f$
102	1 3 11 17 80 18 93 24 101	hpgcom	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f {hp}_{𝒢} (G) (E L D) F$
103	1 3 11 4 79 10 93 98	hpgid	$⊢ φ \to F {hp}_{𝒢} (G) (E L D) F$
104	103	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to F {hp}_{𝒢} (G) (E L D) F$
105	1 3 2 17 25 26 27 20 19 18 11 28 43 24 18 23 73 78 102 104	acopyeu	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f {hl}_{𝒢} (G) (D) F$
106	1 3 23 24 18 19 17 11 105	hlln	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f \in (F L D)$
107	1 3 11 4 10 8 75	tglinerflx1	$⊢ φ \to F \in (F L D)$
108	107	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to F \in (F L D)$
109	1 3 23 4 5 6 7 8 9 10 14	cgrane4	$⊢ φ \to E \neq F$
110	109	ad2antrr	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to E \neq F$
111	1 3 23 24 18 20 17 11 46	hlln	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f \in (F L E)$
112	1 3 11 17 20 18 24 110 111	lncom	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f \in (E L F)$
113	1 3 11 17 20 18 110	tglinerflx2	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to F \in (E L F)$
114	1 3 11 17 18 19 20 18 22 106 108 112 113	tglineinteq	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to f = F$
115	114	oveq2d	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to E \underset{˙}{-} f = E \underset{˙}{-} F$
116	16 115	eqtr3d	$⊢ ((φ \land f \in P) \land (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
117	109	necomd	$⊢ φ \to F \neq E$
118	1 3 23 9 6 7 4 10 2 117 51	hlcgrex	$⊢ φ \to \exists f \in P (f {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} f = B \underset{˙}{-} C)$
119	116 118	r19.29a	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} F$

Metamath Proof Explorer

Theorem tgasa1

Proof