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

Theorem nfn 1954
Description: Inference associated with nfnt 1953. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1880 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 1953 . 2 (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
31, 2ax-mp 5 1 𝑥 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wnf 1879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905
This theorem depends on definitions:  df-bi 199  df-or 875  df-ex 1876  df-nf 1880
This theorem is referenced by:  nfnan  2000  nfor  2004  nfa1  2195  nfna1  2196  nfan1  2232  nfan1OLDOLD  2233  19.32  2268  nfex  2330  cbvexv1  2341  cbvex  2388  cbvex2  2394  nfnae  2418  axc14  2468  sb8vv  2537  euor  2662  euor2  2665  nfne  3069  nfnel  3079  cbvrexf  3347  spcimegf  3473  spcegf  3475  cbvrexcsf  3759  nfdif  3927  rabsnifsb  4444  nfpo  5236  nffr  5284  rexxpf  5471  0neqopab  6930  boxcutc  8189  nfoi  8659  rabssnn0fi  13036  fsuppmapnn0fiubex  13042  sumodd  15444  spc2d  29830  fprodex01  30081  ordtconnlem1  30478  esumrnmpt2  30638  ddemeas  30807  bnj1388  31610  bnj1398  31611  bnj1445  31621  bnj1449  31625  nosupbnd1  32365  nosupbnd2  32367  bj-cbvex2v  33234  finxpreclem6  33723  wl-nfnae1  33798  cdlemefs32sn1aw  36427  ss2iundf  38722  ax6e2ndeqALT  39915  uzwo4  39968  eliin2f  40033  stoweidlem55  41003  stoweidlem59  41007  etransclem32  41214  salexct  41283  sge0f1o  41330  incsmflem  41684  decsmflem  41708  r19.32  41933
  Copyright terms: Public domain W3C validator