Rule of Exportation

Theorem

Formulation 1

$\paren {p \land q} \implies r \dashv \vdash p \implies \paren {q \implies r}$

Formulation 2

$\vdash \paren {\paren {p \land q} \implies r} \iff \paren {p \implies \paren {q \implies r} }$

Also known as

This rule is also known as the rule of shunting.