Biconditional introduction

${\displaystyle \frac{P\to Q,Q\to P}{\therefore P\leftrightarrow Q}}$

where the rule is that wherever instances of "${\displaystyle P\to Q}$" and "${\displaystyle Q\to P}$" appear on lines of a proof, "${\displaystyle P\leftrightarrow Q}$" can validly be placed on a subsequent line.

Formal notation

The biconditional introduction rule may be written in sequent notation:

${\displaystyle (P\to Q),(Q\to P)⊢(P\leftrightarrow Q)}$

where ${\displaystyle ⊢}$ is a metalogical symbol meaning that ${\displaystyle P\leftrightarrow Q}$ is a syntactic consequence when ${\displaystyle P\to Q}$ and ${\displaystyle Q\to P}$ are both in a proof;

or as the statement of a truth-functional tautology or theorem of propositional logic:

${\displaystyle ((P\to Q)\wedge (Q\to P))\to (P\leftrightarrow Q)}$

where ${\displaystyle P}$, and ${\displaystyle Q}$ are propositions expressed in some formal system.