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