Biconditional introduction

In symbolic logic, a valid inference in a system of truth-functional rules. A biconditional sentence is inferred from deriving one side of the sentence (Q) from the assumption of the other (P) in a subproof sequence, followed by a parallel sequence for deriving P from the assumption, Q.