Describes a number of related rules of inference or axiom schema that codify a principle that whenever the truth of $\phi$ entails the truth of $\psi$, then falsity of $\psi$ entails the falsity of $\phi$. Frequently, this rule is described as:

where $\to$ and $\neg$ are conditional and negation connectives, respectively. The term sometimes describes the closely related inference:

or its axiomatic form $(\phi \to \neg \psi )\to (\psi \to \neg \phi )$. These are equivalent in classical logic but are distinct in other deductive systems, such as relevant logic.