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

Theorem nfan1 2199
Description: A closed form of nfan 1898. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1783 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 396 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2 nfim1.1 . . . 4 𝑥𝜑
3 nfim1.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1857 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfim1 2198 . . 3 𝑥(𝜑 → ¬ 𝜓)
65nfn 1856 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
71, 6nfxfr 1852 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wnf 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783
This theorem is referenced by:  sb4b  2479  ralcom2  3376  sbcralt  3871  sbcrext  3872  csbiebt  3927  riota5f  7417  axrepndlem1  10633  axrepndlem2  10634  axunnd  10637  axpowndlem2  10639  axpowndlem3  10640  axpowndlem4  10641  axregndlem2  10644  axinfndlem1  10646  axinfnd  10647  axacndlem4  10651  axacndlem5  10652  axacnd  10653  fproddivf  16024  nfan1c  35088  wl-sbcom2d-lem1  37561  wl-mo2df  37572  wl-eudf  37574  wl-mo3t  37578  wl-ax11-lem4  37590  wl-ax11-lem6  37592
  Copyright terms: Public domain W3C validator