Metamath Proof Explorer


Theorem mvlladdi

Description: Move the left term in a sum on the LHS to the RHS. (Contributed by David A. Wheeler, 11-Oct-2018)

Ref Expression
Hypotheses mvlladdi.1 𝐴 ∈ ℂ
mvlladdi.2 𝐵 ∈ ℂ
mvlladdi.3 ( 𝐴 + 𝐵 ) = 𝐶
Assertion mvlladdi 𝐵 = ( 𝐶𝐴 )

Proof

Step Hyp Ref Expression
1 mvlladdi.1 𝐴 ∈ ℂ
2 mvlladdi.2 𝐵 ∈ ℂ
3 mvlladdi.3 ( 𝐴 + 𝐵 ) = 𝐶
4 2 1 pncan3oi ( ( 𝐵 + 𝐴 ) − 𝐴 ) = 𝐵
5 1 2 3 addcomli ( 𝐵 + 𝐴 ) = 𝐶
6 5 oveq1i ( ( 𝐵 + 𝐴 ) − 𝐴 ) = ( 𝐶𝐴 )
7 4 6 eqtr3i 𝐵 = ( 𝐶𝐴 )