theorem bian12i (a b c d: wff): $ a <-> b /\ c $ > $ d /\ a <-> b /\ (d /\ c) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr | (d /\ a <-> d /\ (b /\ c)) -> (d /\ (b /\ c) <-> b /\ (d /\ c)) -> (d /\ a <-> b /\ (d /\ c)) |
|
| 2 | hyp h | a <-> b /\ c |
|
| 3 | 2 | aneq2i | d /\ a <-> d /\ (b /\ c) |
| 4 | 1, 3 | ax_mp | (d /\ (b /\ c) <-> b /\ (d /\ c)) -> (d /\ a <-> b /\ (d /\ c)) |
| 5 | anlass | d /\ (b /\ c) <-> b /\ (d /\ c) |
|
| 6 | 4, 5 | ax_mp | d /\ a <-> b /\ (d /\ c) |