theorem eqeq (a b c d: nat): $ a = b -> c = d -> (a = c <-> b = d) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anl | a = b /\ c = d -> a = b |
|
| 2 | anr | a = b /\ c = d -> c = d |
|
| 3 | 1, 2 | eqeqd | a = b /\ c = d -> (a = c <-> b = d) |
| 4 | 3 | exp | a = b -> c = d -> (a = c <-> b = d) |