Axiom ax_p3 ≪ | index | src | ≫

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