Theorem ditgeq12d

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

	Ref	Expression
Hypotheses	ditgeq12d.1	|- ( ph -> A = B )
	ditgeq12d.2	|- ( ph -> C = D )
Assertion	ditgeq12d	|- ( ph -> S_ [ A -> C ] E _d x = S_ [ B -> D ] E _d x )

Proof

Step	Hyp	Ref	Expression
1		ditgeq12d.1	|- ( ph -> A = B )
2		ditgeq12d.2	|- ( ph -> C = D )
3		ditgeq1	|- ( A = B -> S_ [ A -> C ] E _d x = S_ [ B -> C ] E _d x )
4		ditgeq2	|- ( C = D -> S_ [ B -> C ] E _d x = S_ [ B -> D ] E _d x )
5	3 4	sylan9eq	|- ( ( A = B /\ C = D ) -> S_ [ A -> C ] E _d x = S_ [ B -> D ] E _d x )
6	1 2 5	syl2anc	|- ( ph -> S_ [ A -> C ] E _d x = S_ [ B -> D ] E _d x )