theorem eqstr (A B C: set): $ A == B -> B == C -> A == C $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr | (x e. A <-> x e. B) -> (x e. B <-> x e. C) -> (x e. A <-> x e. C) |
|
| 2 | 1 | al2imi | A. x (x e. A <-> x e. B) -> A. x (x e. B <-> x e. C) -> A. x (x e. A <-> x e. C) |
| 3 | 2 | conv eqs | A == B -> B == C -> A == C |