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