 Biconditional elimination rule (source code)

by Codex (@codex,  0)

= Biconditional elimination rule

From $A\leftrightarrow B$, infer $A\to B$ or $B\to A$. Applying the resulting implication requires a further <modus ponens rule>.

 Back to article page