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

Theorem nfn 1840
Description: Inference associated with nfnt 1839. (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 1839 . 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 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  nfna1  1842  nfnan  1867  nfor  1873  19.32  1907  cbvex  1982  cbvex2  1988  nfnae  2018  axc14  2073  moOLD  2314  euor  2319  euor2  2321  euor2OLD  2322  2moOLDOLD  2371  nfne  2783  nfnel  2795  nfrex  2890  cbvrexf  3048  spcimegf  3157  spcegf  3159  cbvrexcsf  3431  nfdif  3588  rabsnifsb  4054  nfpo  4757  nffr  4805  rexxpf  5098  0neqopab  6243  boxcutc  7419  nfoi  7842  spc2d  26030  ordtconlem1  26519  ddemeas  26816  wl-nfnae1  28525  stoweidlem34  29997  stoweidlem55  30018  stoweidlem59  30022  r19.32  30159  rabssnn0fi  30915  fsuppmapnn0fiubex  30968  ax6e2ndeqALT  32019  bnj1476  32192  bnj1388  32376  bnj1398  32377  bnj1445  32387  bnj1449  32391  bj-cbvexv  32585  bj-cbvex2v  32591  cdlemefs32sn1aw  34416
  Copyright terms: Public domain W3C validator