MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfn Structured version   Unicode version

Theorem nfn 1956
Description: Inference associated with nfnt 1955. (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 1955 . 2  |-  ( F/ x ph  ->  F/ x  -.  ph )
31, 2ax-mp 5 1  |-  F/ x  -.  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-12 1905
This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664
This theorem is referenced by:  nfna1  1958  nfnan  1985  nfor  1991  19.32  2022  cbvex  2076  cbvex2  2082  nfnae  2113  axc14  2166  euor  2308  euor2  2310  nfne  2756  nfnel  2768  nfrexOLD  2889  cbvrexf  3050  spcimegf  3160  spcegf  3162  cbvrexcsf  3428  nfdif  3586  rabsnifsb  4065  nfpo  4775  nffr  4823  rexxpf  4997  0neqopab  6345  boxcutc  7569  nfoi  8031  rabssnn0fi  12197  fsuppmapnn0fiubex  12203  spc2d  28090  ordtconlem1  28723  esumrnmpt2  28882  ddemeas  29052  bnj1476  29651  bnj1388  29835  bnj1398  29836  bnj1445  29846  bnj1449  29850  bj-cbvexv  31282  bj-cbvex2v  31288  wl-nfnae1  31772  cdlemefs32sn1aw  33897  ss2iundf  36108  ax6e2ndeqALT  37186  uzwo4  37251  stoweidlem34  37712  stoweidlem55  37733  stoweidlem59  37737  etransclem32  37948  sge0f1o  38009  r19.32  38298
  Copyright terms: Public domain W3C validator