theorem bian12da (G a b c d: wff): $ G /\ d -> (a <-> b /\ c) $ > $ G -> (d /\ a <-> b /\ (d /\ c)) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anlass | d /\ (b /\ c) <-> b /\ (d /\ c) |
|
2 | hyp h | G /\ d -> (a <-> b /\ c) |
|
3 | 2 | aneq2da | G -> (d /\ a <-> d /\ (b /\ c)) |
4 | 1, 3 | syl6bb | G -> (d /\ a <-> b /\ (d /\ c)) |