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 = ( invg ` G )
	grpinvinvd.3	|- ( ph -> G e. Grp )
	grpinvinvd.4	|- ( ph -> X e. B )
Assertion	grpinvinvd	|- ( ph -> ( N ` ( N ` X ) ) = X )

Proof

Step	Hyp	Ref	Expression
1		grpinvinvd.1	|- B = ( Base ` G )
2		grpinvinvd.2	|- N = ( invg ` G )
3		grpinvinvd.3	|- ( ph -> G e. Grp )
4		grpinvinvd.4	|- ( ph -> X e. B )
5	1 2	grpinvinv	|- ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )
6	3 4 5	syl2anc	|- ( ph -> ( N ` ( N ` X ) ) = X )