theorem com23 (a b c d: wff): $ a -> b -> c -> d $ > $ a -> c -> b -> d $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpcom | c -> (c -> d) -> d |
|
| 2 | 1 | imim2d | c -> (b -> c -> d) -> b -> d |
| 3 | 2 | com12 | (b -> c -> d) -> c -> b -> d |
| 4 | hyp h | a -> b -> c -> d |
|
| 5 | 3, 4 | syl | a -> c -> b -> d |