Biconditional introduction

In propositional logic, biconditional introduction is a valid rule of inference. It makes it possible to introduce a biconditional into a logical proof. If the statement that A implies B and also the statement that B implies A both appear in a proof, then one may introduce the statement A if and only if B or formally, (A ↔ B).

For example, from the statements "if I'm breathing, then I'm alive" and "if I'm alive, then I'm breathing", it can be inferred that "I'm breathing if and only if I'm alive".

Formally, biconditional introduction is the rule schema.

$A\to B\,$

${\underline {B\to A}}$

$A\leftrightarrow B$