Description: Move the left term in a sum on the LHS to the RHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mvlraddd.1 | |- ( ph -> A e. CC ) |
|
mvlraddd.2 | |- ( ph -> B e. CC ) |
||
mvlraddd.3 | |- ( ph -> ( A + B ) = C ) |
||
Assertion | mvlladdd | |- ( ph -> B = ( C - A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mvlraddd.1 | |- ( ph -> A e. CC ) |
|
2 | mvlraddd.2 | |- ( ph -> B e. CC ) |
|
3 | mvlraddd.3 | |- ( ph -> ( A + B ) = C ) |
|
4 | 2 1 | pncand | |- ( ph -> ( ( B + A ) - A ) = B ) |
5 | 1 2 | addcomd | |- ( ph -> ( A + B ) = ( B + A ) ) |
6 | 5 3 | eqtr3d | |- ( ph -> ( B + A ) = C ) |
7 | 6 | oveq1d | |- ( ph -> ( ( B + A ) - A ) = ( C - A ) ) |
8 | 4 7 | eqtr3d | |- ( ph -> B = ( C - A ) ) |