Axiom ax_3 | index | src |

Axiom 3 of Lukasiewicz' axioms for classical propositional logic.

axiom ax_3 (a b: wff): $ (~a -> ~b) -> b -> a $;