Biconditional Elimination - Formal Notation

Formal Notation

The biconditional elimination rule may be written in sequent notation:

and

where is a metalogical symbol meaning that, in the first case, and in the other are syntactic consequences of in some logical system;

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

where, and are propositions expressed in some formal system.