theorem biim1a (a b: wff): $ (~a -> b) -> (a -> b <-> b) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anr | (~a -> b) /\ (a -> b) -> a -> b |
|
| 2 | anl | (~a -> b) /\ (a -> b) -> ~a -> b |
|
| 3 | 1, 2 | casesd | (~a -> b) /\ (a -> b) -> b |
| 4 | 3 | exp | (~a -> b) -> (a -> b) -> b |
| 5 | ax_1 | b -> a -> b |
|
| 6 | 5 | a1i | (~a -> b) -> b -> a -> b |
| 7 | 4, 6 | ibid | (~a -> b) -> (a -> b <-> b) |