Theorem ditgeq12i

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

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

Proof

Step	Hyp	Ref	Expression
1		ditgeq12i.1	$$⊢A=B$$
2		ditgeq12i.2	$$⊢C=D$$
3		eqid	$$⊢E=E$$
4	1 2 3	ditgeq123i	$$⊢{\int }_A^{C}Edx={\int }_B^{D}Edx$$