In propositional logic, biconditional introduction[1][2][3] is a valid rule of inference.

It allows for one to infer a biconditional from two conditional statements.

The rule makes it possible to introduce a biconditional statement into a logical proof.

" can validly be placed on a subsequent line.

The biconditional introduction rule may be written in sequent notation: where

is a metalogical symbol meaning that

are both in a proof; or as the statement of a truth-functional tautology or theorem of propositional logic: where

are propositions expressed in some formal system.