Biconditional elimination

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

Biconditional elimination allows one to infer a conditional from a biconditional: if ( A ↔ B ) is true, then one may infer either direction of the biconditional, ( A → B ) and ( B → A ).

For example, if it's true that I'm breathing if and only if I'm alive, then it's true that if I'm breathing, I'm alive; likewise, it's true that if I'm alive, I'm breathing.

Formally:

$\frac{( A \leftrightarrow B )}{\therefore ( A \rightarrow B )}$

also

$\frac{( A \leftrightarrow B )}{\therefore ( B \rightarrow A )}$

See also

• Logical biconditional
• If and only if