This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpinvinvd

Description: Double inverse law for groups. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses grpinvinvd.1 ⊢ B = Base G
grpinvinvd.2 ⊢ N = inv g ⁡ G
grpinvinvd.3 ⊢ φ → G ∈ Grp
grpinvinvd.4 ⊢ φ → X ∈ B
Assertion grpinvinvd ⊢ φ → N ⁡ N ⁡ X = X

Proof

Step Hyp Ref Expression
1 grpinvinvd.1 ⊢ B = Base G
2 grpinvinvd.2 ⊢ N = inv g ⁡ G
3 grpinvinvd.3 ⊢ φ → G ∈ Grp
4 grpinvinvd.4 ⊢ φ → X ∈ B
5 1 2 grpinvinv ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ N ⁡ X = X
6 3 4 5 syl2anc ⊢ φ → N ⁡ N ⁡ X = X