Exportation[1][2][3][4] is a valid rule of replacement in propositional logic.

The rule allows conditional statements having conjunctive antecedents to be replaced by statements having conditional consequents and vice versa in logical proofs.

" is a metalogical symbol representing "can be replaced in a proof with."

The exportation rule may be written in sequent notation: where

is a metalogical symbol meaning that

" appears on a line of a proof, it can be replaced with "

Import-export is a name given to the statement as a theorem or truth-functional tautology of propositional logic: where

are propositions expressed in some logical system.

At any time, if P→Q is true, it can be replaced by P→(P∧Q).

Another possible case sets P as false and Q as true.

The last case occurs when both P and Q are false.

It rains and the sun shines implies that there is a rainbow.

Thus, if it rains, then the sun shines implies that there is a rainbow.

The following proof uses a classically valid chain of equivalences.

Rules used are material implication, De Morgan's law, and the associative property of conjunction.

Exportation is associated with currying via the Curry–Howard correspondence.