Deduction theorem for propositional logic ($S\cup \{\varphi \}⊢\psi ⟺S⊢\varphi \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.