Metamath Proof Explorer


Theorem mvrladdi

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

Ref Expression
Hypotheses mvrladdi.1
|- B e. CC
mvrladdi.2
|- C e. CC
mvrladdi.3
|- A = ( B + C )
Assertion mvrladdi
|- ( A - B ) = C

Proof

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