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
|- A e. CC
mvlladdi.2
|- B e. CC
mvlladdi.3
|- ( A + B ) = C
Assertion mvlladdi
|- B = ( C - A )

Proof

Step Hyp Ref Expression
1 mvlladdi.1
 |-  A e. CC
2 mvlladdi.2
 |-  B e. CC
3 mvlladdi.3
 |-  ( A + B ) = C
4 2 1 pncan3oi
 |-  ( ( B + A ) - A ) = B
5 1 2 3 addcomli
 |-  ( B + A ) = C
6 5 oveq1i
 |-  ( ( B + A ) - A ) = ( C - A )
7 4 6 eqtr3i
 |-  B = ( C - A )