Axiom ax_1 ≪ | index | src | ≫

axiom ax_1 (A B: wff): $ A \imp B \imp A $;