Axiom 1 of Lukasiewicz' axioms for classical propositional logic.
axiom ax_1 (a b: wff): $ a -> b -> a $;