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

Metamath Proof Explorer

Theorem grpridd

Description: The identity element of a group is a right identity. Deduction associated with grprid . (Contributed by SN, 29-Jan-2025)

Step	Hyp	Ref	Expression
1		grpbn0.b	$⊢ B = {Base}_{G}$
2		grplid.p	$⊢ \underset{˙}{+} = +_{G}$
3		grplid.o	$⊢ \underset{˙}{0} = 0_{G}$
4		grplidd.g	$⊢ φ \to G \in Grp$
5		grplidd.1	$⊢ φ \to X \in B$
6	1 2 3	grprid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} \underset{˙}{0} = X$
7	4 5 6	syl2anc	$⊢ φ \to X \underset{˙}{+} \underset{˙}{0} = X$