Theorem ngen | index | src |

theorem ngen {x: nat} (a: wff x): $ ~a $ > $ ~E. x a $;
StepHypRefExpression
1 notnot1
A. x ~a -> ~~A. x ~a
2 1 conv ex
A. x ~a -> ~E. x a
3 hyp h
~a
4 3 ax_gen
A. x ~a
5 2, 4 ax_mp
~E. x a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen)