theorem bitr3g (a b c d e: wff): $ b <-> d $ > $ c <-> e $ > $ a -> (b <-> c) $ > $ a -> (d <-> e) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicom | (b <-> d) -> (d <-> b) |
|
2 | hyp h1 | b <-> d |
|
3 | 1, 2 | ax_mp | d <-> b |
4 | hyp h2 | c <-> e |
|
5 | hyp h | a -> (b <-> c) |
|
6 | 4, 5 | syl6bb | a -> (b <-> e) |
7 | 3, 6 | syl5bb | a -> (d <-> e) |