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