theorem oreqi (a b c d: wff): $ a <-> b $ > $ c <-> d $ > $ a \/ c <-> b \/ d $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr | (a \/ c <-> b \/ c) -> (b \/ c <-> b \/ d) -> (a \/ c <-> b \/ d) |
|
| 2 | hyp h1 | a <-> b |
|
| 3 | 2 | oreq1i | a \/ c <-> b \/ c |
| 4 | 1, 3 | ax_mp | (b \/ c <-> b \/ d) -> (a \/ c <-> b \/ d) |
| 5 | hyp h2 | c <-> d |
|
| 6 | 5 | oreq2i | b \/ c <-> b \/ d |
| 7 | 4, 6 | ax_mp | a \/ c <-> b \/ d |