Metamath Proof Explorer


Theorem nex

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

Ref Expression
Hypothesis nex.1 ¬ φ
Assertion nex ¬ x φ

Proof

Step Hyp Ref Expression
1 nex.1 ¬ φ
2 alnex x ¬ φ ¬ x φ
3 2 1 mpgbi ¬ x φ