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

Theorem nfn 1853
Description: Inference associated with nfnt 1852. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1779 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 1852 . 2 (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
31, 2ax-mp 5 1 𝑥 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wnf 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-or 846  df-ex 1775  df-nf 1779
This theorem is referenced by:  nfnan  1896  nfor  1900  nfnaewOLD  2139  nfa1  2141  nfna1  2142  nfan1  2189  19.32  2222  nfex  2313  cbvexv1  2333  cbvex2v  2335  cbvex  2393  cbvex2  2406  nfnae  2428  axc14  2457  euor  2600  euor2  2602  nfne  3033  nfnel  3044  cbvrexfw  3293  cbvrexf  3345  ceqsex  3513  spcimegf  3575  spcegf  3577  spc2d  3587  cbvrexcsf  3937  nfdif  4121  nfdifOLD  4122  rabsnifsb  4721  0nelopabOLD  5564  nfpo  5589  nffr  5646  rexxpf  5844  boxcutc  8959  nfoi  9547  rabssnn0fi  13997  fsuppmapnn0fiubex  14003  sumodd  16382  nosupbnd1  27738  nosupbnd2  27740  noinfbnd1  27753  noinfbnd2  27755  fprodex01  32726  ordtconnlem1  33749  esumrnmpt2  33911  ddemeas  34079  bnj1388  34888  bnj1398  34889  bnj1445  34899  bnj1449  34903  finxpreclem6  37113  wl-nfnae1  37233  cdlemefs32sn1aw  40123  nfa1w  42365  ss2iundf  43360  ax6e2ndeqALT  44641  uzwo4  44688  eliin2f  44739  stoweidlem55  45709  stoweidlem59  45713  etransclem32  45920  salexct  45988  sge0f1o  46036  incsmflem  46395  decsmflem  46420  r19.32  46744
  Copyright terms: Public domain W3C validator