Theorem grpassd

Description: A group operation is associative. (Contributed by SN, 29-Jan-2025)

	Ref	Expression
Hypotheses	grpassd.b	|- B = ( Base ` G )
	grpassd.p	|- .+ = ( +g ` G )
	grpassd.g	|- ( ph -> G e. Grp )
	grpassd.1	|- ( ph -> X e. B )
	grpassd.2	|- ( ph -> Y e. B )
	grpassd.3	|- ( ph -> Z e. B )
Assertion	grpassd	|- ( ph -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		grpassd.b	|- B = ( Base ` G )
2		grpassd.p	|- .+ = ( +g ` G )
3		grpassd.g	|- ( ph -> G e. Grp )
4		grpassd.1	|- ( ph -> X e. B )
5		grpassd.2	|- ( ph -> Y e. B )
6		grpassd.3	|- ( ph -> Z e. B )
7	1 2	grpass	|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
8	3 4 5 6 7	syl13anc	|- ( ph -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )