nex - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > nex		Unicode version

Theorem nex 1555

Description: Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)

**Hypothesis**
Ref	Expression
nex.1

**Assertion**
Ref	Expression
nex

**Proof of Theorem nex**
Step	Hyp	Ref	Expression
1		alnex 1543	. 2
2		nex.1	. 2
3	1, 2	mpgbi 1549	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wex 1541

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

This theorem depends on definitions: df-bi 177 df-ex 1542

This theorem is referenced by: ru 3046 0nel1c 4160 xp0r 4843 dm0 4919 co02 5093 co01 5094 nenpw1pwlem2 6086