Theorem itgeq2sdv

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

	Ref	Expression
Hypothesis	itgeq2sdv.1	⊢ ( 𝜑 → 𝐵 = 𝐶 )
Assertion	itgeq2sdv	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 𝐶 d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		itgeq2sdv.1	⊢ ( 𝜑 → 𝐵 = 𝐶 )
2		eqidd	⊢ ( 𝜑 → 𝐴 = 𝐴 )
3	2 1	itgeq12sdv	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 𝐶 d 𝑥 )