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

Theorem nfn 1824
Description: Inference associated with nfnt 1822. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1750 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 1822 . 2 (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
31, 2ax-mp 5 1 𝑥 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1745  df-nf 1750
This theorem is referenced by:  nfanOLD  1869  nfnan  1870  nfor  1874  nfa1  2068  nfna1  2069  nfan1  2106  19.32  2139  nfex  2192  cbvexv1  2212  cbvex  2308  cbvex2  2316  nfnae  2351  axc14  2400  euor  2541  euor2  2543  nfne  2923  nfnel  2933  cbvrexf  3196  spcimegf  3318  spcegf  3320  cbvrexcsf  3599  nfdif  3764  rabsnifsb  4289  nfpo  5069  nffr  5117  rexxpf  5302  0neqopab  6740  boxcutc  7993  nfoi  8460  rabssnn0fi  12825  fsuppmapnn0fiubex  12832  sumodd  15158  spc2d  29441  fprodex01  29699  ordtconnlem1  30098  esumrnmpt2  30258  ddemeas  30427  bnj1388  31227  bnj1398  31228  bnj1445  31238  bnj1449  31242  nosupbnd1  31985  nosupbnd2  31987  bj-cbvex2v  32863  finxpreclem6  33363  wl-nfnae1  33446  cdlemefs32sn1aw  36019  ss2iundf  38268  ax6e2ndeqALT  39481  uzwo4  39535  eliin2f  39601  stoweidlem55  40590  stoweidlem59  40594  etransclem32  40801  salexct  40870  sge0f1o  40917  incsmflem  41271  decsmflem  41295  r19.32  41488
  Copyright terms: Public domain W3C validator