theorem oreq1a (a b c: wff): $ (~c -> (a <-> b)) -> (a \/ c <-> b \/ c) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orcomb | a \/ c <-> c \/ a |
|
| 2 | orcomb | c \/ b <-> b \/ c |
|
| 3 | oreq2a | (~c -> (a <-> b)) -> (c \/ a <-> c \/ b) |
|
| 4 | 2, 3 | syl6bb | (~c -> (a <-> b)) -> (c \/ a <-> b \/ c) |
| 5 | 1, 4 | syl5bb | (~c -> (a <-> b)) -> (a \/ c <-> b \/ c) |