Theorem notfal ≪ | index | src | ≫ 

theorem notfal: $ ~F. $;
StepHypRefExpression
1 notnot1 
T. -> ~~T.
2 1 conv fal 
T. -> ~F.
3 itru 
T.
4 2, 3 ax_mp 
~F.

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru)