theorem ifppos2 (a b c: wff): $ b -> (ifp a b c <-> a \/ c) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oreq2a | (~a -> (~a /\ c <-> c)) -> (a \/ ~a /\ c <-> a \/ c) |
|
| 2 | bian1 | ~a -> (~a /\ c <-> c) |
|
| 3 | 1, 2 | ax_mp | a \/ ~a /\ c <-> a \/ c |
| 4 | bian2 | b -> (a /\ b <-> a) |
|
| 5 | 4 | oreq1d | b -> (a /\ b \/ ~a /\ c <-> a \/ ~a /\ c) |
| 6 | 5 | conv ifp | b -> (ifp a b c <-> a \/ ~a /\ c) |
| 7 | 3, 6 | syl6bb | b -> (ifp a b c <-> a \/ c) |