theorem eqeq2 (a b c: nat): $ b = c -> (a = b <-> a = c) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqtr | a = b -> b = c -> a = c |
|
| 2 | 1 | com12 | b = c -> a = b -> a = c |
| 3 | eqtr4 | a = c -> b = c -> a = b |
|
| 4 | 3 | com12 | b = c -> a = c -> a = b |
| 5 | 2, 4 | ibid | b = c -> (a = b <-> a = c) |