theorem con4b (a b: wff): $ (~a <-> ~b) -> (a <-> b) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bi2 | (~a <-> ~b) -> ~b -> ~a |
|
| 2 | 1 | con4d | (~a <-> ~b) -> a -> b |
| 3 | bi1 | (~a <-> ~b) -> ~a -> ~b |
|
| 4 | 3 | con4d | (~a <-> ~b) -> b -> a |
| 5 | 2, 4 | ibid | (~a <-> ~b) -> (a <-> b) |