Theorem mulgcld

Description: Deduction associated with mulgcl . (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	mulgcld.1	|- B = ( Base ` G )
	mulgcld.2	|- .x. = ( .g ` G )
	mulgcld.3	|- ( ph -> G e. Grp )
	mulgcld.4	|- ( ph -> N e. ZZ )
	mulgcld.5	|- ( ph -> X e. B )
Assertion	mulgcld	|- ( ph -> ( N .x. X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		mulgcld.1	|- B = ( Base ` G )
2		mulgcld.2	|- .x. = ( .g ` G )
3		mulgcld.3	|- ( ph -> G e. Grp )
4		mulgcld.4	|- ( ph -> N e. ZZ )
5		mulgcld.5	|- ( ph -> X e. B )
6	1 2	mulgcl	|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B )
7	3 4 5 6	syl3anc	|- ( ph -> ( N .x. X ) e. B )