Metamath Proof Explorer

Theorem itgeq2sdv

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

Ref Expression
Hypothesis itgeq2sdv.1 
|- ( ph -> B = C )
Assertion itgeq2sdv 
|- ( ph -> S. A B _d x = S. A C _d x )

Proof

Step Hyp Ref Expression
1 itgeq2sdv.1 
 |-  ( ph -> B = C )
2 eqidd 
 |-  ( ph -> A = A )
3 2 1 itgeq12sdv 
 |-  ( ph -> S. A B _d x = S. A C _d x )