ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfn GIF version

Theorem nfn 1651
Description: Inference associated with nfnt 1649. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfn.1 𝑥𝜑
Assertion
Ref Expression
nfn 𝑥 ¬ 𝜑

Proof of Theorem nfn
StepHypRef Expression
1 nfn.1 . 2 𝑥𝜑
2 nfnt 1649 . 2 (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
31, 2ax-mp 5 1 𝑥 ¬ 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wnf 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ie2 1487  ax-4 1503  ax-ial 1527
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-fal 1354  df-nf 1454
This theorem is referenced by:  nfdc  1652  19.32dc  1672  nfnae  1715  mo2n  2047  nfne  2433  nfnel  2442  nfdif  3248  nfpo  4286  0neqopab  5898  nfsup  6969  ismkvnex  7131  mkvprop  7134  zsupcllemstep  11900  oddpwdclemndvds  12125  ismkvnnlem  14084
  Copyright terms: Public domain W3C validator