theorem notan (a b: wff): $ ~(a /\ b) <-> ~a \/ ~b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr | (~(a /\ b) <-> a -> ~b) -> (a -> ~b <-> ~a \/ ~b) -> (~(a /\ b) <-> ~a \/ ~b) |
|
| 2 | notan2 | ~(a /\ b) <-> a -> ~b |
|
| 3 | 1, 2 | ax_mp | (a -> ~b <-> ~a \/ ~b) -> (~(a /\ b) <-> ~a \/ ~b) |
| 4 | notnot | a <-> ~~a |
|
| 5 | 4 | imeq1i | a -> ~b <-> ~~a -> ~b |
| 6 | 5 | conv or | a -> ~b <-> ~a \/ ~b |
| 7 | 3, 6 | ax_mp | ~(a /\ b) <-> ~a \/ ~b |