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¬φ