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