Theorem leacgra

Description: GeoCoq l11__30 analogue: leA is preserved when both compared angles are replaced by congruent angles. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	leacgra.p	$$⊢P={\mathrm{Base}}_G$$
	leacgra.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	leacgra.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	leacgra.s	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}^{\angle }\left(G\right)$$
	leacgra.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	leacgra.a	$$⊢\phi \to A\in P$$
	leacgra.b	$$⊢\phi \to B\in P$$
	leacgra.c	$$⊢\phi \to C\in P$$
	leacgra.d	$$⊢\phi \to D\in P$$
	leacgra.e	$$⊢\phi \to E\in P$$
	leacgra.f	$$⊢\phi \to F\in P$$
	leacgra.h	$$⊢\phi \to H\in P$$
	leacgra.u	$$⊢\phi \to U\in P$$
	leacgra.j	$$⊢\phi \to J\in P$$
	leacgra.x	$$⊢\phi \to X\in P$$
	leacgra.y	$$⊢\phi \to Y\in P$$
	leacgra.z	$$⊢\phi \to Z\in P$$
	leacgra.1	$$⊢\phi \to ⟨“ABC”⟩\underset{\dot{}}{\le }⟨“DEF”⟩$$
	leacgra.2	$$⊢\phi \to ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“HUJ”⟩$$
	leacgra.3	$$⊢\phi \to ⟨“DEF”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“XYZ”⟩$$
Assertion	leacgra	$$⊢\phi \to ⟨“HUJ”⟩\underset{\dot{}}{\le }⟨“XYZ”⟩$$

Proof

Step	Hyp	Ref	Expression
1		leacgra.p	$$⊢P={\mathrm{Base}}_G$$
2		leacgra.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		leacgra.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
4		leacgra.s	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}^{\angle }\left(G\right)$$
5		leacgra.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		leacgra.a	$$⊢\phi \to A\in P$$
7		leacgra.b	$$⊢\phi \to B\in P$$
8		leacgra.c	$$⊢\phi \to C\in P$$
9		leacgra.d	$$⊢\phi \to D\in P$$
10		leacgra.e	$$⊢\phi \to E\in P$$
11		leacgra.f	$$⊢\phi \to F\in P$$
12		leacgra.h	$$⊢\phi \to H\in P$$
13		leacgra.u	$$⊢\phi \to U\in P$$
14		leacgra.j	$$⊢\phi \to J\in P$$
15		leacgra.x	$$⊢\phi \to X\in P$$
16		leacgra.y	$$⊢\phi \to Y\in P$$
17		leacgra.z	$$⊢\phi \to Z\in P$$
18		leacgra.1	$$⊢\phi \to ⟨“ABC”⟩\underset{\dot{}}{\le }⟨“DEF”⟩$$
19		leacgra.2	$$⊢\phi \to ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“HUJ”⟩$$
20		leacgra.3	$$⊢\phi \to ⟨“DEF”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“XYZ”⟩$$
21	4	breqi	$$⊢⟨“ABC”⟩\underset{\dot{}}{\le }⟨“DEF”⟩\leftrightarrow ⟨“ABC”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩$$
22	18 21	sylib	$$⊢\phi \to ⟨“ABC”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩$$
23	1 2 3 5 6 7 8 9 10 11 12 13 14 22 19	leacgra1	$$⊢\phi \to ⟨“HUJ”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩$$
24	1 2 3 5 12 13 14 9 10 11 15 16 17 23 20	leacgra2	$$⊢\phi \to ⟨“HUJ”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“XYZ”⟩$$
25	4	breqi	$$⊢⟨“HUJ”⟩\underset{\dot{}}{\le }⟨“XYZ”⟩\leftrightarrow ⟨“HUJ”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“XYZ”⟩$$
26	24 25	sylibr	$$⊢\phi \to ⟨“HUJ”⟩\underset{\dot{}}{\le }⟨“XYZ”⟩$$