Metamath Proof Explorer


Theorem nfn

Description: Inference associated with nfnt . (Contributed by Mario Carneiro, 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 nfn.1 x φ
2 nfnt x φ x ¬ φ
3 1 2 ax-mp x ¬ φ