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 |
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 |