Exportation

The logical equivalence that transforms a conditional with a conjunction antecedent into a nested conditional: (A ∧ B) → C is equivalent to A → (B → C). In type-theoretic and computational readings this corresponds to currying, the isomorphism between functions of two arguments and curried functions.