Theorem tgaas

Description: Angle-angle-side: two triangles with two congruent angles and a congruent side not included between them are congruent. The side included between the two angles is congruent by tgaas1 , which reduces the theorem to SAS ( tgsas ). (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgaas1.p	|- P = ( Base ` G )
	tgaas1.m	|- .- = ( dist ` G )
	tgaas1.i	|- I = ( Itv ` G )
	tgaas1.l	|- L = ( LineG ` G )
	tgaas1.g	|- ( ph -> G e. TarskiG )
	tgaas1.a	|- ( ph -> A e. P )
	tgaas1.b	|- ( ph -> B e. P )
	tgaas1.c	|- ( ph -> C e. P )
	tgaas1.d	|- ( ph -> D e. P )
	tgaas1.e	|- ( ph -> E e. P )
	tgaas1.f	|- ( ph -> F e. P )
	tgaas1.ncol	|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
	tgaas1.1	|- ( ph -> ( A .- B ) = ( D .- E ) )
	tgaas1.2	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
	tgaas1.3	|- ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )
Assertion	tgaas	|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E F "> )

Proof

Step	Hyp	Ref	Expression
1		tgaas1.p	|- P = ( Base ` G )
2		tgaas1.m	|- .- = ( dist ` G )
3		tgaas1.i	|- I = ( Itv ` G )
4		tgaas1.l	|- L = ( LineG ` G )
5		tgaas1.g	|- ( ph -> G e. TarskiG )
6		tgaas1.a	|- ( ph -> A e. P )
7		tgaas1.b	|- ( ph -> B e. P )
8		tgaas1.c	|- ( ph -> C e. P )
9		tgaas1.d	|- ( ph -> D e. P )
10		tgaas1.e	|- ( ph -> E e. P )
11		tgaas1.f	|- ( ph -> F e. P )
12		tgaas1.ncol	|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
13		tgaas1.1	|- ( ph -> ( A .- B ) = ( D .- E ) )
14		tgaas1.2	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
15		tgaas1.3	|- ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	tgaas1	|- ( ph -> ( B .- C ) = ( E .- F ) )
17	1 2 3 5 6 7 8 9 10 11 13 14 16	tgsas	|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E F "> )