Metamath Proof Explorer


Theorem nexdv

Description: Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993) Reduce dependencies on axioms. (Revised by Wolf Lammen, 13-Jul-2020) (Proof shortened by Wolf Lammen, 10-Oct-2021)

Ref Expression
Hypothesis nexdv.1 φ¬ψ
Assertion nexdv φ¬xψ

Proof

Step Hyp Ref Expression
1 nexdv.1 φ¬ψ
2 ax-5 φxφ
3 2 1 nexdh φ¬xψ