Theorem itgeq2sdv

Description: Equality theorem for an integral. Deduction form. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypothesis	itgeq2sdv.1	$$⊢\phi \to B=C$$
Assertion	itgeq2sdv	$$⊢\phi \to {\int }_{A}Bdx={\int }_{A}Cdx$$

Proof

Step	Hyp	Ref	Expression
1		itgeq2sdv.1	$$⊢\phi \to B=C$$
2		eqidd	$$⊢\phi \to A=A$$
3	2 1	itgeq12sdv	$$⊢\phi \to {\int }_{A}Bdx={\int }_{A}Cdx$$