Description: Swap the second and third variables in an equation with subtraction on the left, converting it into an addition.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 23-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lsubswap23d.a | |- ( ph -> A e. CC ) |
|
| lsubswap23d.b | |- ( ph -> B e. CC ) |
||
| lsubswap23d.1 | |- ( ph -> ( A - B ) = C ) |
||
| Assertion | lsubswap23d | |- ( ph -> ( A - C ) = B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lsubswap23d.a | |- ( ph -> A e. CC ) |
|
| 2 | lsubswap23d.b | |- ( ph -> B e. CC ) |
|
| 3 | lsubswap23d.1 | |- ( ph -> ( A - B ) = C ) |
|
| 4 | 1 2 | subcld | |- ( ph -> ( A - B ) e. CC ) |
| 5 | 3 4 | eqeltrrd | |- ( ph -> C e. CC ) |
| 6 | 1 5 | subcld | |- ( ph -> ( A - C ) e. CC ) |
| 7 | 4 3 | subeq0bd | |- ( ph -> ( ( A - B ) - C ) = 0 ) |
| 8 | 1 5 2 | sub32d | |- ( ph -> ( ( A - C ) - B ) = ( ( A - B ) - C ) ) |
| 9 | 2 | subidd | |- ( ph -> ( B - B ) = 0 ) |
| 10 | 7 8 9 | 3eqtr4d | |- ( ph -> ( ( A - C ) - B ) = ( B - B ) ) |
| 11 | 6 2 2 10 | subcan2d | |- ( ph -> ( A - C ) = B ) |