theorem imim (a b c d: wff): $ (a -> b) -> (c -> d) -> (b -> c) -> a -> d $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim2 | (c -> d) -> (b -> c) -> b -> d |
|
2 | imim1 | (a -> b) -> (b -> d) -> a -> d |
|
3 | 2 | imim2d | (a -> b) -> ((b -> c) -> b -> d) -> (b -> c) -> a -> d |
4 | 1, 3 | syl5 | (a -> b) -> (c -> d) -> (b -> c) -> a -> d |