Theorem prodeq12si

Description: Equality inference for product. General version of prodeq2si . (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	prodeq12si.1	|- A = B
	prodeq12si.2	|- C = D
Assertion	prodeq12si	|- prod_ x e. A C = prod_ x e. B D

Proof

Step	Hyp	Ref	Expression
1		prodeq12si.1	|- A = B
2		prodeq12si.2	|- C = D
3	1	prodeq1i	|- prod_ x e. A C = prod_ x e. B C
4	2	prodeq2si	|- prod_ x e. B C = prod_ x e. B D
5	3 4	eqtri	|- prod_ x e. A C = prod_ x e. B D