Theorem ditgeq12d

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

	Ref	Expression
Hypotheses	ditgeq12d.1	$$⊢\phi \to A=B$$
	ditgeq12d.2	$$⊢\phi \to C=D$$
Assertion	ditgeq12d	$$⊢\phi \to {\int }_A^{C}Edx={\int }_B^{D}Edx$$

Proof

Step	Hyp	Ref	Expression
1		ditgeq12d.1	$$⊢\phi \to A=B$$
2		ditgeq12d.2	$$⊢\phi \to C=D$$
3		ditgeq1	$$⊢A=B\to {\int }_A^{C}Edx={\int }_B^{C}Edx$$
4		ditgeq2	$$⊢C=D\to {\int }_B^{C}Edx={\int }_B^{D}Edx$$
5	3 4	sylan9eq	$$⊢\left(A=B\wedge C=D\right)\to {\int }_A^{C}Edx={\int }_B^{D}Edx$$
6	1 2 5	syl2anc	$$⊢\phi \to {\int }_A^{C}Edx={\int }_B^{D}Edx$$