Metamath Proof Explorer

Theorem itgeq2i

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

Ref Expression
Hypothesis itgeq2i.1 
|- B = C
Assertion itgeq2i 
|- S. A B _d x = S. A C _d x

Proof

Step Hyp Ref Expression
1 itgeq2i.1 
 |-  B = C
2 eqid 
 |-  A = A
3 2 1 itgeq12i 
 |-  S. A B _d x = S. A C _d x