Theorem ablcomd

Description: An abelian group operation is commutative, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	ablcomd.1	|- B = ( Base ` G )
	ablcomd.2	|- .+ = ( +g ` G )
	ablcomd.3	|- ( ph -> G e. Abel )
	ablcomd.4	|- ( ph -> X e. B )
	ablcomd.5	|- ( ph -> Y e. B )
Assertion	ablcomd	|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )

Proof

Step	Hyp	Ref	Expression
1		ablcomd.1	|- B = ( Base ` G )
2		ablcomd.2	|- .+ = ( +g ` G )
3		ablcomd.3	|- ( ph -> G e. Abel )
4		ablcomd.4	|- ( ph -> X e. B )
5		ablcomd.5	|- ( ph -> Y e. B )
6	1 2	ablcom	|- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
7	3 4 5 6	syl3anc	|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )