Theorem nex 1099

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

Syntax hints:  -. wn 2  E.wex 978

This theorem is referenced by:  ru 1934  rab0 2289  axnul2 2703  notzfaus 2736  dtrucor2 2769  xp0r 3234  0nelxp 3235  dm0 3318  dmsn0 3319  dmsnsn0 3320  co02 3500  oarec 4186  0nelqs 4288  canth2 4470  brdom3 4781  cfsuc 4895  ivthlem8 7231  ivthlem8OLD 7240  ruc 7500

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

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

Copyright terms: Public domain