theorem eqeqd (G: wff) (a b c d: nat): $ G -> a = b $ > $ G -> c = d $ > $ G -> (a = c <-> b = d) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h1 | G -> a = b |
|
2 | 1 | eqeq1d | G -> (a = c <-> b = c) |
3 | hyp h2 | G -> c = d |
|
4 | 3 | eqeq2d | G -> (b = c <-> b = d) |
5 | 2, 4 | bitrd | G -> (a = c <-> b = d) |