Axiom ax_p1 ≪ | index | src | ≫

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