Axiom ax_3 ≪ | index | src | ≫

axiom ax_3 (A B: wff): $ (\neg A \imp \neg B) \imp B \imp A $;