Theorem nexdv 1864

Description: Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 13-Jul-2020.) (Proof shortened by Wolf Lammen, 10-Oct-2021.)

Hypothesis

Ref	Expression
nexdv.1	|- ( ph -> -. ps )

Assertion

Ref	Expression
nexdv	|- ( ph -> -. E. x ps )

Distinct variable group:   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem nexdv

Step	Hyp	Ref	Expression
1		ax-5 1839	. 2 |- ( ph -> A. x ph )
2		nexdv.1	. 2 |- ( ph -> -. ps )
3	1, 2	nexdh 1792	1 |- ( ph -> -. E. x ps )

Syntax hints:   -. wn 3   -> wi 4   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  sbc2or  3444  csbopab  5008  relimasn  5488  csbiota  5881  canthwdom  8484  cfsuc  9079  ssfin4  9132  konigthlem  9390  axunndlem1  9417  canthnum  9471  canthwe  9473  pwfseq  9486  tskuni  9605  ptcmplem4  21859  lgsquadlem3  25107  umgredgnlp  26042  dfrdg4  32058