Biconditional Introduction

From ProofWiki
Jump to navigation Jump to search

Proof Rule

The rule of biconditional introduction is a valid deduction sequent in propositional logic.


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.


Also see