Description: Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd with a commuted consequent, and of mvlraddd with a commuted hypothesis.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | raddswap12d.b | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | |
| raddswap12d.c | ⊢ ( 𝜑 → 𝐶 ∈ ℂ ) | ||
| raddswap12d.1 | ⊢ ( 𝜑 → 𝐴 = ( 𝐵 + 𝐶 ) ) | ||
| Assertion | raddswap12d | ⊢ ( 𝜑 → 𝐵 = ( 𝐴 − 𝐶 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | raddswap12d.b | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | |
| 2 | raddswap12d.c | ⊢ ( 𝜑 → 𝐶 ∈ ℂ ) | |
| 3 | raddswap12d.1 | ⊢ ( 𝜑 → 𝐴 = ( 𝐵 + 𝐶 ) ) | |
| 4 | 1 2 3 | mvrraddd | ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = 𝐵 ) |
| 5 | 4 | eqcomd | ⊢ ( 𝜑 → 𝐵 = ( 𝐴 − 𝐶 ) ) |