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

Theorem nfn 1849
Description: Inference associated with nfnt 1848. (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 1848 . 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 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600
This theorem is referenced by:  nfna1  1851  nfnan  1876  nfor  1882  19.32  1916  cbvex  1995  cbvex2  2001  nfnae  2031  axc14  2086  moOLD  2327  euor  2332  euor2  2334  euor2OLD  2335  2moOLDOLD  2384  nfne  2798  nfnel  2810  nfrexOLD  2928  cbvrexf  3083  spcimegf  3192  spcegf  3194  cbvrexcsf  3468  nfdif  3625  rabsnifsb  4095  nfpo  4805  nffr  4853  rexxpf  5150  0neqopab  6326  boxcutc  7513  nfoi  7940  rabssnn0fi  12064  fsuppmapnn0fiubex  12067  spc2d  27146  ordtconlem1  27657  ddemeas  27959  wl-nfnae1  29834  stoweidlem34  31561  stoweidlem55  31582  stoweidlem59  31586  r19.32  31866  ax6e2ndeqALT  33028  bnj1476  33201  bnj1388  33385  bnj1398  33386  bnj1445  33396  bnj1449  33400  bj-cbvexv  33596  bj-cbvex2v  33602  cdlemefs32sn1aw  35427
  Copyright terms: Public domain W3C validator