pub theorem ifpneg (p a b: wff): $ ~p -> (ifp p a b <-> b) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bior1 | ~(p /\ a) -> (p /\ a \/ ~p /\ b <-> ~p /\ b) |
|
| 2 | 1 | conv ifp | ~(p /\ a) -> (ifp p a b <-> ~p /\ b) |
| 3 | con3 | (p /\ a -> p) -> ~p -> ~(p /\ a) |
|
| 4 | anl | p /\ a -> p |
|
| 5 | 3, 4 | ax_mp | ~p -> ~(p /\ a) |
| 6 | 2, 5 | syl | ~p -> (ifp p a b <-> ~p /\ b) |
| 7 | bian1 | ~p -> (~p /\ b <-> b) |
|
| 8 | 6, 7 | bitrd | ~p -> (ifp p a b <-> b) |