Axiom ax_1 index | src |

Axiom 1 of Lukasiewicz' axioms for classical propositional logic.

axiom ax_1 (a b: wff): $ a -> b -> a $;