theorem eqsub1 (a b c: nat): $ a + b = c -> c - b = a $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq1 | a + b = b + a -> (a + b = c <-> b + a = c) |
|
| 2 | addcom | a + b = b + a |
|
| 3 | 1, 2 | ax_mp | a + b = c <-> b + a = c |
| 4 | eqsub2 | b + a = c -> c - b = a |
|
| 5 | 3, 4 | sylbi | a + b = c -> c - b = a |