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

Theorem nfan1 2193
Description: A closed form of nfan 1902. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1786 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 7-Jul-2022.)
Hypotheses
Ref Expression
nfim1.1 𝑥𝜑
nfim1.2 (𝜑 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nfan1 𝑥(𝜑𝜓)

Proof of Theorem nfan1
StepHypRef Expression
1 df-an 397 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2 nfim1.1 . . . 4 𝑥𝜑
3 nfim1.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1861 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfim1 2192 . . 3 𝑥(𝜑 → ¬ 𝜓)
65nfn 1860 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
71, 6nfxfr 1855 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786
This theorem is referenced by:  sb4b  2474  ralcom2  3373  sbcralt  3866  sbcrext  3867  csbiebt  3923  riota5f  7393  axrepndlem1  10586  axrepndlem2  10587  axunnd  10590  axpowndlem2  10592  axpowndlem3  10593  axpowndlem4  10594  axregndlem2  10597  axinfndlem1  10599  axinfnd  10600  axacndlem4  10604  axacndlem5  10605  axacnd  10606  fproddivf  15930  wl-sbcom2d-lem1  36419  wl-mo2df  36430  wl-eudf  36432  wl-mo3t  36436  wl-ax11-lem4  36445  wl-ax11-lem6  36447
  Copyright terms: Public domain W3C validator