Metamath Proof Explorer


Theorem mvrraddi

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

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

Proof

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