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

Theorem nfn 1848
Description: Inference associated with nfnt 1847. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1776 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 1847 . 2 (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
31, 2ax-mp 5 1 𝑥 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-or 842  df-ex 1772  df-nf 1776
This theorem is referenced by:  nfnan  1892  nfor  1896  nfnaew  2144  nfa1  2146  nfna1  2147  nfan1  2191  19.32  2226  nfex  2335  cbvexv1  2354  cbvex2v  2357  cbvex  2411  cbvex2  2428  nfnae  2451  axc14  2481  euor  2691  euor2  2693  nfne  3119  nfnel  3130  cbvrexfw  3439  cbvrexf  3441  spcimegf  3589  spcegf  3591  spc2d  3602  cbvrexcsf  3925  nfdif  4101  rabsnifsb  4652  0nelopab  5444  nfpo  5473  nffr  5523  rexxpf  5712  boxcutc  8494  nfoi  8967  rabssnn0fi  13344  fsuppmapnn0fiubex  13350  sumodd  15729  fprodex01  30469  ordtconnlem1  31067  esumrnmpt2  31227  ddemeas  31395  bnj1388  32203  bnj1398  32204  bnj1445  32214  bnj1449  32218  nosupbnd1  33112  nosupbnd2  33114  finxpreclem6  34560  wl-nfnae1  34651  cdlemefs32sn1aw  37432  ss2iundf  39884  ax6e2ndeqALT  41145  uzwo4  41195  eliin2f  41251  stoweidlem55  42221  stoweidlem59  42225  etransclem32  42432  salexct  42498  sge0f1o  42545  incsmflem  42899  decsmflem  42923  r19.32  43177
  Copyright terms: Public domain W3C validator