Theorem inotda ≪ | index | src | ≫ 

theorem inotda (a b: wff): $ a /\ b -> ~b $ > $ a -> ~b $;
StepHypRefExpression
1 inot 
(b -> ~b) -> ~b
2 hyp h 
a /\ b -> ~b
3 1, 2 syla 
a -> ~b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)