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