# Biconditional Introduction

Jump to navigation
Jump to search

## Proof Rule

The **rule of biconditional introduction** is a valid argument in types of logic dealing with conditionals $\implies$ and biconditionals $\iff$.

This includes classical propositional logic and predicate logic, and in particular natural deduction.

### Proof Rule

- If we can conclude both $\phi \implies \psi$ and $\psi \implies \phi$, then we may infer $\phi \iff \psi$.

### Sequent Form

- $p \implies q, q \implies p \vdash p \iff q$

## Also known as

Some sources refer to the Biconditional Introduction as the rule of **Conditional-Biconditional**.