Biconditional introduction

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