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 1785 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 1784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810
This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1781  df-nf 1785
This theorem is referenced by:  nfnan  1901  nfor  1905  nfa1  2156  nfna1  2157  nfan1  2205  19.32  2238  nfex  2327  cbvexv1  2344  cbvex2v  2346  cbvex  2401  cbvex2  2414  nfnae  2436  axc14  2465  euor  2608  euor2  2610  nfne  3030  nfnel  3041  cbvrexfw  3274  cbvrexf  3328  ceqsex  3486  spcimegf  3505  spcegf  3543  spc2d  3553  cbvrexcsf  3889  nfdif  4078  nfdifOLD  4079  rabsnifsb  4674  nfpo  5533  nffr  5592  rexxpf  5791  boxcutc  8871  nfoi  9407  rabssnn0fi  13895  fsuppmapnn0fiubex  13901  sumodd  16301  nosupbnd1  27654  nosupbnd2  27656  noinfbnd1  27669  noinfbnd2  27671  fprodex01  32813  ordtconnlem1  33958  esumrnmpt2  34102  ddemeas  34270  bnj1388  35066  bnj1398  35067  bnj1445  35077  bnj1449  35081  finxpreclem6  37461  wl-nfnae1  37593  cdlemefs32sn1aw  40533  ss2iundf  43776  ax6e2ndeqALT  45047  uzwo4  45174  eliin2f  45225  stoweidlem55  46177  stoweidlem59  46181  etransclem32  46388  salexct  46456  sge0f1o  46504  incsmflem  46863  decsmflem  46888  r19.32  47222
  Copyright terms: Public domain W3C validator