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 | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
| tgaas1.m | ⊢ − = ( dist ‘ 𝐺 ) | ||
| tgaas1.i | ⊢ 𝐼 = ( Itv ‘ 𝐺 ) | ||
| tgaas1.l | ⊢ 𝐿 = ( LineG ‘ 𝐺 ) | ||
| tgaas1.g | ⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) | ||
| tgaas1.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | ||
| tgaas1.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) | ||
| tgaas1.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) | ||
| tgaas1.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 ) | ||
| tgaas1.e | ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 ) | ||
| tgaas1.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 ) | ||
| tgaas1.ncol | ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) | ||
| tgaas1.1 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ) | ||
| tgaas1.2 | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) | ||
| tgaas1.3 | ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) | ||
| Assertion | tgaas | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tgaas1.p | ⊢ 𝑃 = ( Base ‘ 𝐺 ) | |
| 2 | tgaas1.m | ⊢ − = ( dist ‘ 𝐺 ) | |
| 3 | tgaas1.i | ⊢ 𝐼 = ( Itv ‘ 𝐺 ) | |
| 4 | tgaas1.l | ⊢ 𝐿 = ( LineG ‘ 𝐺 ) | |
| 5 | tgaas1.g | ⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) | |
| 6 | tgaas1.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | |
| 7 | tgaas1.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) | |
| 8 | tgaas1.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) | |
| 9 | tgaas1.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 ) | |
| 10 | tgaas1.e | ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 ) | |
| 11 | tgaas1.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 ) | |
| 12 | tgaas1.ncol | ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) | |
| 13 | tgaas1.1 | ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ) | |
| 14 | tgaas1.2 | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) | |
| 15 | tgaas1.3 | ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ ) | |
| 16 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 | tgaas1 | ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) ) |
| 17 | 1 2 3 5 6 7 8 9 10 11 13 14 16 | tgsas | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) |