theorem iman (a b: wff): $ a -> b <-> ~(a /\ ~b) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr4 | (a -> b <-> a -> ~~b) -> (~(a /\ ~b) <-> a -> ~~b) -> (a -> b <-> ~(a /\ ~b)) |
|
| 2 | notnot | b <-> ~~b |
|
| 3 | 2 | imeq2i | a -> b <-> a -> ~~b |
| 4 | 1, 3 | ax_mp | (~(a /\ ~b) <-> a -> ~~b) -> (a -> b <-> ~(a /\ ~b)) |
| 5 | notan2 | ~(a /\ ~b) <-> a -> ~~b |
|
| 6 | 4, 5 | ax_mp | a -> b <-> ~(a /\ ~b) |