Axiom ax_p2 ≪ | index | src | ≫

axiom ax_p2 (A B C: wff): $ (A \imp B \imp C) \imp (A \imp B) \imp A \imp C $;