Theorem nex 1137

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

Syntax hints:  -. wn 2  E.wex 1016

This theorem is referenced by:  ru 1984  rab0 2346  axnul2 2782  notzfaus 2815  dtrucor2 2850  xp0r 3325  0nelxp 3326  dm0 3414  co02 3612  oarec 4332  canth2 4629  brdom3 4947  cfsuc 5065  ivthlem8 7493  ruc 7761  fsubbas 11630

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

This theorem depends on definitions:  df-bi 145  df-ex 1017

Copyright terms: Public domain