The results in this section are based on implication only, and avoid ax-3,
so are intuitionistic. The system { ax-mp, ax-1, ax-2 } axiomatizes
what is sometimes called "intuitionistic implicational calculus" or "minimal
implicational calculus".
In an implication, the wff before the arrow is called the "antecedent" and
the wff after the arrow is called the "consequent".