Theorem ditgeq3sdv

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

	Ref	Expression
Hypothesis	ditgeq3sdv.1	|- ( ph -> C = D )
Assertion	ditgeq3sdv	|- ( ph -> S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d x )

Proof

Step	Hyp	Ref	Expression
1		ditgeq3sdv.1	|- ( ph -> C = D )
2		eqidd	|- ( ph -> A = A )
3		eqidd	|- ( ph -> B = B )
4	2 3 1	ditgeq123dv	|- ( ph -> S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d x )