Theorem nexi | index | src |

theorem nexi {x: nat} (a: wff x): $ ~a $ > $ ~E. x a $;
StepHypRefExpression
1 alnex
A. x ~a <-> ~E. x a
2 hyp h
~a
3 2 ax_gen
A. x ~a
4 1, 3 mpbi
~E. x a

Axiom use

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