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 ⊢ ∫ A B dx = ∫ A C dx

Proof

Step Hyp Ref Expression
1 itgeq2i.1 ⊢ B = C
2 eqid ⊢ A = A
3 2 1 itgeq12i ⊢ ∫ A B dx = ∫ A C dx