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

Theorem nfn 1838
Description: Inference associated with nfnt 1837. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1766 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 1837 . 2 (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
31, 2ax-mp 5 1 𝑥 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wnf 1765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791
This theorem depends on definitions:  df-bi 208  df-or 843  df-ex 1762  df-nf 1766
This theorem is referenced by:  nfnan  1882  nfor  1886  nfa1  2121  nfna1  2122  nfan1  2165  19.32  2200  nfex  2306  cbvexv1  2321  cbvex  2373  cbvex2  2390  nfnae  2413  axc14  2443  euor  2662  euor2  2665  nfne  3087  nfnel  3097  cbvrexf  3398  spcimegf  3532  spcegf  3534  spc2d  3545  cbvrexcsf  3850  nfdif  4023  rabsnifsb  4565  0nelopab  5340  nfpo  5367  nffr  5417  rexxpf  5604  boxcutc  8353  nfoi  8824  rabssnn0fi  13204  fsuppmapnn0fiubex  13210  sumodd  15572  fprodex01  30225  ordtconnlem1  30784  esumrnmpt2  30944  ddemeas  31112  bnj1388  31919  bnj1398  31920  bnj1445  31930  bnj1449  31934  nosupbnd1  32823  nosupbnd2  32825  bj-cbvex2v  33669  finxpreclem6  34208  wl-nfnae1  34301  cdlemefs32sn1aw  37081  ss2iundf  39489  ax6e2ndeqALT  40804  uzwo4  40854  eliin2f  40910  stoweidlem55  41882  stoweidlem59  41886  etransclem32  42093  salexct  42159  sge0f1o  42206  incsmflem  42560  decsmflem  42584  r19.32  42812
  Copyright terms: Public domain W3C validator