theorem imeq1a (a b c: wff): $ (~c -> (a <-> b)) -> (a -> c <-> b -> c) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con3bi | a -> c <-> ~c -> ~a |
|
| 2 | con3bi | b -> c <-> ~c -> ~b |
|
| 3 | imeq2a | (~c -> (~a <-> ~b)) -> (~c -> ~a <-> ~c -> ~b) |
|
| 4 | noteq | (a <-> b) -> (~a <-> ~b) |
|
| 5 | 4 | imim2i | (~c -> (a <-> b)) -> ~c -> (~a <-> ~b) |
| 6 | 3, 5 | syl | (~c -> (a <-> b)) -> (~c -> ~a <-> ~c -> ~b) |
| 7 | 1, 2, 6 | bitr4g | (~c -> (a <-> b)) -> (a -> c <-> b -> c) |