Deduction theorem for propositional logic
= Deduction theorem for propositional logic
{title2=$S\cup\{\phi\}\vdash\psi\iff S\vdash\phi\Rightarrow\psi$}
An implication is derivable from a theory precisely when its conclusion is derivable after adjoining its antecedent. Together with classical contradiction rules, this identifies failure to prove a proposition with consistency after adjoining its negation.