theorem imeq2a (a b c: wff): $ (a -> (b <-> c)) -> (a -> b <-> a -> c) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bi1 | (b <-> c) -> b -> c |
|
| 2 | 1 | imim2i | (a -> (b <-> c)) -> a -> b -> c |
| 3 | 2 | a2d | (a -> (b <-> c)) -> (a -> b) -> a -> c |
| 4 | bi2 | (b <-> c) -> c -> b |
|
| 5 | 4 | imim2i | (a -> (b <-> c)) -> a -> c -> b |
| 6 | 5 | a2d | (a -> (b <-> c)) -> (a -> c) -> a -> b |
| 7 | 3, 6 | ibid | (a -> (b <-> c)) -> (a -> b <-> a -> c) |