Biconditional introduction

Rules of inference
Propositional calculus
Modus ponens Modus tollens Modus ponendo tollens Conjunction introduction Simplification Disjunction introduction Disjunction elimination Disjunctive syllogism Hypothetical syllogism Constructive dilemma Destructive dilemma Biconditional introduction Biconditional elimination
Predicate calculus
Universal generalization Universal instantiation Existential generalization Existential instantiation

In mathematical logic, biconditional introduction is the rule of inference that, if B follows from A, and A follows from B, then A if and only if 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$

See also

• Logical biconditional