theorem biim2a (a b: wff): $ (b -> ~a) -> (a -> b <-> ~a) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inot | (a -> ~a) -> ~a |
|
| 2 | imim2 | (b -> ~a) -> (a -> b) -> a -> ~a |
|
| 3 | 2 | imp | (b -> ~a) /\ (a -> b) -> a -> ~a |
| 4 | 1, 3 | syl | (b -> ~a) /\ (a -> b) -> ~a |
| 5 | 4 | exp | (b -> ~a) -> (a -> b) -> ~a |
| 6 | absurd | ~a -> a -> b |
|
| 7 | 6 | a1i | (b -> ~a) -> ~a -> a -> b |
| 8 | 5, 7 | ibid | (b -> ~a) -> (a -> b <-> ~a) |