Biconditional Introduction - Formal Notation

Formal Notation

The biconditional introduction rule may be written in sequent notation:

where is a metalogical symbol meaning that is a syntactic consequence when and are both in a proof;

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

where, and are propositions expressed in some formal system.