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

Theorem nfn 1858
Description: Inference associated with nfnt 1857. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1786 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
Hypothesis
Ref Expression
nfn.1 𝑥𝜑
Assertion
Ref Expression
nfn 𝑥 ¬ 𝜑

Proof of Theorem nfn
StepHypRef Expression
1 nfn.1 . 2 𝑥𝜑
2 nfnt 1857 . 2 (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
31, 2ax-mp 5 1 𝑥 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786
This theorem is referenced by:  nfnan  1901  nfor  1905  nfnaew  2151  nfa1  2153  nfna1  2154  nfan1  2199  19.32  2234  nfex  2335  cbvexv1  2354  cbvex2v  2357  cbvex  2409  cbvex2  2426  nfnae  2448  axc14  2478  euor  2675  euor2  2677  nfne  3090  nfnel  3101  cbvrexfw  3387  cbvrexf  3389  spcimegf  3540  spcegf  3542  spc2d  3554  cbvrexcsf  3874  nfdif  4056  rabsnifsb  4621  0nelopab  5420  nfpo  5447  nffr  5497  rexxpf  5686  boxcutc  8492  nfoi  8966  rabssnn0fi  13353  fsuppmapnn0fiubex  13359  sumodd  15732  fprodex01  30570  ordtconnlem1  31275  esumrnmpt2  31435  ddemeas  31603  bnj1388  32413  bnj1398  32414  bnj1445  32424  bnj1449  32428  nosupbnd1  33322  nosupbnd2  33324  finxpreclem6  34808  wl-nfnae1  34926  cdlemefs32sn1aw  37703  ss2iundf  40347  ax6e2ndeqALT  41624  uzwo4  41674  eliin2f  41727  stoweidlem55  42684  stoweidlem59  42688  etransclem32  42895  salexct  42961  sge0f1o  43008  incsmflem  43362  decsmflem  43386  r19.32  43640
  Copyright terms: Public domain W3C validator