Theorem ditgeq3sdv

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

	Ref	Expression
Hypothesis	ditgeq3sdv.1	$$⊢\phi \to C=D$$
Assertion	ditgeq3sdv	$$⊢\phi \to {\int }_A^{B}Cdx={\int }_A^{B}Ddx$$

Proof

Step	Hyp	Ref	Expression
1		ditgeq3sdv.1	$$⊢\phi \to C=D$$
2		eqidd	$$⊢\phi \to A=A$$
3		eqidd	$$⊢\phi \to B=B$$
4	2 3 1	ditgeq123dv	$$⊢\phi \to {\int }_A^{B}Cdx={\int }_A^{B}Ddx$$