Theorem nexd | index | src |

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

Axiom use

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