Theorem nex 1456

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 1380	. 2 |- (A.x -. ph <-> -. E.xph)
2		nex.1	. 2 |- -. ph
3	1, 2	mpgbi 1333	1 |- -. E.xph

Syntax hints:  -. wn 2  E.wex 1326

This theorem is referenced by:  ru 2451  rab0OLD 2895  axnulALT 3443  notzfaus 3478  dtrucor2 3519  xp0r 4065  0nelxp 4066  dm0 4170  dm0OLD 4171  co02 4411  oarec 5244  canth2 5548  brdom3 5963  cfsuc 6063  ivthlem8 8550  ruc 8818  fsubbas 10281  bnj1419 13117  nextnt 14155  nextf 14156  unqsym1 14249  amosym1 14250  subsym1 14251

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

This theorem depends on definitions:  df-bi 164  df-ex 1327

Copyright terms: Public domain