Biconditional elimination

ψ)、(φ → χ)和(ψ → χ)可推出χ。 双条件介入（英语：Biconditional introduction）：从(φ → ψ)和(ψ → φ)中可推出(φ ↔ ψ)。 双条件除去（英语：Biconditional elimination）：从(φ ↔ ψ)中可推出(φ → ψ)和(ψ → φ)。