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