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

Theorem nfn 1658
Description: Inference associated with nfnt 1656. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfn.1  |-  F/ x ph
Assertion
Ref Expression
nfn  |-  F/ x  -.  ph

Proof of Theorem nfn
StepHypRef Expression
1 nfn.1 . 2  |-  F/ x ph
2 nfnt 1656 . 2  |-  ( F/ x ph  ->  F/ x  -.  ph )
31, 2ax-mp 5 1  |-  F/ x  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   F/wnf 1460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ie2 1494  ax-4 1510  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-fal 1359  df-nf 1461
This theorem is referenced by:  nfdc  1659  19.32dc  1679  nfnae  1722  mo2n  2054  nfne  2440  nfnel  2449  nfdif  3256  nfpo  4301  0neqopab  5919  nfsup  6990  ismkvnex  7152  mkvprop  7155  zsupcllemstep  11945  oddpwdclemndvds  12170  ismkvnnlem  14770
  Copyright terms: Public domain W3C validator