Theorem nfn 1710

Description: Inference associated with nfnt 1708. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfn.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfn	⊢ Ⅎ𝑥 ¬ 𝜑

Proof of Theorem nfn

Step	Hyp	Ref	Expression
1		nfn.1	. 2 ⊢ Ⅎ𝑥𝜑
2		nfnt 1708	. 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
3	1, 2	ax-mp 5	1 ⊢ Ⅎ𝑥 ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3  Ⅎwnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-4 1563  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-tru 1405  df-fal 1408  df-nf 1514

This theorem is used by:  nfdc  1711  19.32dc  1731  nfnae  1774  mo2n  2114  nfne  2513  nfnel  2522  nfdif  3350  rabsnifsb  3777  nfpo  4446  0neqopab  6133  nfsup  7333  ismkvnex  7496  mkvprop  7499  zsupcllemstep  10673  nnmaxpwlemndvds  12969  ismkvnnlem  17269