Theorem ditgeq3sdv

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

	Ref	Expression
Hypothesis	ditgeq3sdv.1	⊢ ( 𝜑 → 𝐶 = 𝐷 )
Assertion	ditgeq3sdv	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		ditgeq3sdv.1	⊢ ( 𝜑 → 𝐶 = 𝐷 )
2		eqidd	⊢ ( 𝜑 → 𝐴 = 𝐴 )
3		eqidd	⊢ ( 𝜑 → 𝐵 = 𝐵 )
4	2 3 1	ditgeq123dv	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 )