# Metamath Proof Explorer

## Theorem iseqlgd

Description: Condition for a triangle to be equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020)

Ref Expression
Hypotheses iseqlg.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
iseqlg.m
iseqlg.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
iseqlg.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
iseqlg.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
iseqlg.a ${⊢}{\phi }\to {A}\in {P}$
iseqlg.b ${⊢}{\phi }\to {B}\in {P}$
iseqlg.c ${⊢}{\phi }\to {C}\in {P}$
iseqlgd.1
iseqlgd.2
iseqlgd.3
Assertion iseqlgd ${⊢}{\phi }\to ⟨“{A}{B}{C}”⟩\in {Equilaterals}_{𝒢}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 iseqlg.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 iseqlg.m
3 iseqlg.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 iseqlg.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
5 iseqlg.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
6 iseqlg.a ${⊢}{\phi }\to {A}\in {P}$
7 iseqlg.b ${⊢}{\phi }\to {B}\in {P}$
8 iseqlg.c ${⊢}{\phi }\to {C}\in {P}$
9 iseqlgd.1
10 iseqlgd.2
11 iseqlgd.3
12 eqid ${⊢}{\sim }_{𝒢}\left({G}\right)={\sim }_{𝒢}\left({G}\right)$
13 1 2 12 5 6 7 8 7 8 6 9 10 11 trgcgr ${⊢}{\phi }\to ⟨“{A}{B}{C}”⟩{\sim }_{𝒢}\left({G}\right)⟨“{B}{C}{A}”⟩$
14 1 2 3 4 5 6 7 8 iseqlg ${⊢}{\phi }\to \left(⟨“{A}{B}{C}”⟩\in {Equilaterals}_{𝒢}\left({G}\right)↔⟨“{A}{B}{C}”⟩{\sim }_{𝒢}\left({G}\right)⟨“{B}{C}{A}”⟩\right)$
15 13 14 mpbird ${⊢}{\phi }\to ⟨“{A}{B}{C}”⟩\in {Equilaterals}_{𝒢}\left({G}\right)$