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