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

Theorem nfn 1906
Description: Inference associated with nfnt 1905. (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 1905 . 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 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622
This theorem is referenced by:  nfna1  1908  nfnan  1934  nfor  1940  19.32  1972  cbvex  2027  cbvex2  2033  nfnae  2062  axc14  2115  euor  2330  euor2  2332  nfne  2785  nfnel  2797  nfrexOLD  2918  cbvrexf  3076  spcimegf  3185  spcegf  3187  cbvrexcsf  3453  nfdif  3611  rabsnifsb  4084  nfpo  4794  nffr  4842  rexxpf  5139  0neqopab  6314  boxcutc  7505  nfoi  7931  rabssnn0fi  12080  fsuppmapnn0fiubex  12083  spc2d  27574  ordtconlem1  28144  esumrnmpt2  28300  ddemeas  28448  wl-nfnae1  30224  stoweidlem34  32058  stoweidlem55  32079  stoweidlem59  32083  etransclem32  32291  r19.32  32414  ax6e2ndeqALT  34151  bnj1476  34325  bnj1388  34509  bnj1398  34510  bnj1445  34520  bnj1449  34524  bj-cbvexv  34717  bj-cbvex2v  34723  cdlemefs32sn1aw  36556
  Copyright terms: Public domain W3C validator