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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nexdv.1 | |
|
2 | ax-5 | |
|
3 | 2 1 | nexdh | |