Theorem nex 1097

Description: Generalization rule for negated wff.

Hypothesis

Ref	Expression
nex.1	|- -. ph

Assertion

Ref	Expression
nex	|- -. E.xph

Proof of Theorem nex

Step	Hyp	Ref	Expression
1		alnex 1029	. 2 |- (A.x -. ph <-> -. E.xph)
2		nex.1	. 2 |- -. ph
3	1, 2	mpgbi 984	1 |- -. E.xph

Syntax hints:  -. wn 2  E.wex 977

This theorem is referenced by:  ru 1928  rab0 2283  axnul2 2698  notzfaus 2731  dtrucor2 2764  xp0r 3229  0nelxp 3230  dm0 3312  dmsn0 3313  dmsnsn0 3314  co02 3494  oarec 4180  0nelqs 4282  canth2 4464  brdom3 4773  cfsuc 4887  ivthlem8 7223  ivthlem8OLD 7232  ruc 7492

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960

This theorem depends on definitions:  df-bi 147  df-ex 978

Copyright terms: Public domain