The question of whether the Import-Export principle can be derived from, or is even compatible with, varieties of logic with conditionals other than material implication has been quite a live topic in the logic of conditionals in recent years. So, this is an interesting question.
First, to make the symbols clearer, I'll use → for material implication and > for some as-yet-undetermined conditional that more closely reflects the meaning of 'if' in English. I'll use ↔ for the material biconditional. I will say that the > conditional collapses into material implication if it is possible to prove both that A > B entails A → B and also A → B entails A > B. The general version of Import-Export can then be stated as:
⊨ (A > (B > C)) ↔ ((A ∧ B) > C)
The Import-Export principle, when used with some other simple logical principles causes any conditional to collapse into material implication. For example, Allan Gibbard showed that we get collapse if we accept Modus Ponens, Import-Export, and a principle called Left Logical Equivalence, which holds that A ↔ B entails (A > C) ↔ (B > C). Several logicians have proposed weaker logics in order to avoid this conclusion. Vann McGee has argued for exceptions to Modus Ponens; a bunch of logicians have argued against Left Logical Equivalence; and a bunch more have argued that Import-Export is not correct in the general case.
Mandelkern (2020) shows that if have Import-Export and a classical understanding of conjunction, then again we get collapse. In Mandelkern (2021) he shows that we also get collapse if we combine Import-Export with the Identity Principle, ⊨ A > A, a reductio type principle he calls Triviality: {A > B, A > ¬B} ⊨ ¬A and another he calls Very Weak Monotonicity. Mandelkern's conclusion is that Import-Export is not compatible with a non-material implication understanding of conditionals and so Import-Export should not be considered valid.
It should perhaps not surprise us that Import-Export does not work universally. If we substitute A for C, then (A ∧ B) > A is not equivalent to A > (B > A). The former is a logical truth, while the latter is doubtful in some cases. Also, Import-Export does not always hold for counterfactual conditionals. Consequently, Import-Export does not hold in accounts of conditionals such as the variably strict account of Stalnaker.
The upshot is that it is more difficult than one might suppose to avoid material implication. Classical logic is a coherent whole, and changing the conditional requires either a change in the rules of inference, including Import-Export, or a change in the meaning of the other connectives: and, or, not, which leads in the direction of a non-classical logic. This is not to say I am defending material implication. I'm not: it is an extremely crude approximation to the meaning of 'if'. But working around it is a lot of work, and might even require a distinctly different logic from classical.
Allan Gibbard, “Two Recent Theories of Conditionals”, in Harper, Stalnaker, and Pearce (eds.), IFS: Conditionals, Belief, Decision, Chance and Time, pp. 211–247 (1980).
Matthew Mandelkern, "Import-Export and 'And'", Philosophy and Phenomenological Research, 100, pp. 118-135 (2020).
Matthew Mandelkern, "If p, then p!", Journal of Philosophy 118, pp. 645-679 (2021).
