Biconditional introduction is a rule of inference in sentential logic that says if you know that P => Q and Q => P then you may conclude P <=> Q.
Biconditional elimination is another rule of inference in sentential logic that says if you know P <=> Q, you may conclude P => Q. Likewise, you can conclude Q => P.
Both of these rules of inference are almost entirely definitional, so they should be straightforward.