Theorem absurd | index | src |

theorem absurd (a b: wff): $ ~a -> a -> b $;
StepHypRefExpression
1 ax_1
~a -> ~b -> ~a
2 1 a3d
~a -> a -> b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)