theorem bitr3gi (a b c d: wff): $ a <-> c $ > $ b <-> d $ > $ a <-> b $ > $ c <-> d $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr3 | (a <-> c) -> (a <-> d) -> (c <-> d) |
|
| 2 | hyp h1 | a <-> c |
|
| 3 | 1, 2 | ax_mp | (a <-> d) -> (c <-> d) |
| 4 | bitr | (a <-> b) -> (b <-> d) -> (a <-> d) |
|
| 5 | hyp h | a <-> b |
|
| 6 | 4, 5 | ax_mp | (b <-> d) -> (a <-> d) |
| 7 | hyp h2 | b <-> d |
|
| 8 | 6, 7 | ax_mp | a <-> d |
| 9 | 3, 8 | ax_mp | c <-> d |