Theorem absurdr | index | src |

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

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)