I've wondered about this. The book for my logic course (now done with) had no rule for creating equivalences. If you had A <--> B, by the system in the book you couldn't replace occurrences of A with B and occurrences of B with A. You'd have to break down A <--> B with material equivalence and work from there. Is there any particular reason for that?