theorem imeqi (a b c d: wff): $ a <-> b $ > $ c <-> d $ > $ a -> c <-> b -> d $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr | (a -> c <-> b -> c) -> (b -> c <-> b -> d) -> (a -> c <-> b -> d) |
|
| 2 | hyp h1 | a <-> b |
|
| 3 | 2 | imeq1i | a -> c <-> b -> c |
| 4 | 1, 3 | ax_mp | (b -> c <-> b -> d) -> (a -> c <-> b -> d) |
| 5 | hyp h2 | c <-> d |
|
| 6 | 5 | imeq2i | b -> c <-> b -> d |
| 7 | 4, 6 | ax_mp | a -> c <-> b -> d |