Theorem 2cprodeq2dv

Description: Equality deduction for double product. (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Hypothesis	2cprodeq2dv.1	|- ( ( ph /\ j e. A /\ k e. B ) -> C = D )
Assertion	2cprodeq2dv	|- ( ph -> prod_ j e. A prod_ k e. B C = prod_ j e. A prod_ k e. B D )

Proof

Step	Hyp	Ref	Expression
1		2cprodeq2dv.1	|- ( ( ph /\ j e. A /\ k e. B ) -> C = D )
2	1	3expa	|- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C = D )
3	2	prodeq2dv	|- ( ( ph /\ j e. A ) -> prod_ k e. B C = prod_ k e. B D )
4	3	prodeq2dv	|- ( ph -> prod_ j e. A prod_ k e. B C = prod_ j e. A prod_ k e. B D )