theorem bitrd (a b c d: wff): $ a -> (b <-> c) $ > $ a -> (c <-> d) $ > $ a -> (b <-> d) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h1 | a -> (b <-> c) |
|
| 2 | 1 | bi1d | a -> b -> c |
| 3 | hyp h2 | a -> (c <-> d) |
|
| 4 | 3 | bi1d | a -> c -> d |
| 5 | 2, 4 | syld | a -> b -> d |
| 6 | 3 | bi2d | a -> d -> c |
| 7 | 1 | bi2d | a -> c -> b |
| 8 | 6, 7 | syld | a -> d -> b |
| 9 | 5, 8 | ibid | a -> (b <-> d) |