Axiom ax_mp index | src | ≫

axiom ax_mp (A B: wff): $ A \imp B $ > $ A $ > $ B $;