Import–export (logic)

In propositional logic, import-export is a name given to the propositional form of Exportation:

${\displaystyle (P\rightarrow (Q\rightarrow R))\leftrightarrow ((P\land Q)\rightarrow R)}$.

This already holds in minimal logic, and thus also in classical logic, where the conditional operator "${\displaystyle \rightarrow }$" is taken as material implication. In the Curry-Howard correspondence for intuitionistic logics, it can be realized through currying and uncurrying.