theorem ifpneg3 (a b c: wff): $ ~c -> (ifp a b c <-> a /\ b) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bior2 | ~(~a /\ c) -> (a /\ b \/ ~a /\ c <-> a /\ b) |
|
| 2 | 1 | conv ifp | ~(~a /\ c) -> (ifp a b c <-> a /\ b) |
| 3 | con3 | (~a /\ c -> c) -> ~c -> ~(~a /\ c) |
|
| 4 | anr | ~a /\ c -> c |
|
| 5 | 3, 4 | ax_mp | ~c -> ~(~a /\ c) |
| 6 | 2, 5 | syl | ~c -> (ifp a b c <-> a /\ b) |