# Biconditional elimination

Transformation rules |
---|

Propositional calculus |

Rules of inference |

Rules of replacement |

Predicate logic |

**Biconditional elimination** is the name of two valid rules of inference of propositional logic. It allows for one to infer a conditional from a biconditional. If is true, then one may infer that is true, and also that is true.^{[1]} 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. The rules can be stated formally as:

and

where the rule is that wherever an instance of "" appears on a line of a proof, either "" or "" can be placed on a subsequent line;

## Formal notation[edit]

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.

## See also[edit]

## References[edit]

**^**Cohen, S. Marc. "Chapter 8: The Logic of Conditionals" (PDF). University of Washington. Retrieved 8 October 2013.