theorem bior1a (a b: wff): $ (a -> b) -> (a \/ b <-> b) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | notnot | a <-> ~~a |
|
| 2 | 1 | imeq1i | a -> b <-> ~~a -> b |
| 3 | biim1a | (~~a -> b) -> (~a -> b <-> b) |
|
| 4 | 3 | conv or | (~~a -> b) -> (a \/ b <-> b) |
| 5 | 2, 4 | sylbi | (a -> b) -> (a \/ b <-> b) |