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

Theorem nfan1 2200
Description: A closed form of nfan 1899. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1784 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 1858 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfim1 2199 . . 3 𝑥(𝜑 → ¬ 𝜓)
65nfn 1857 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
71, 6nfxfr 1853 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784
This theorem is referenced by:  sb4b  2480  ralcom2  3377  sbcralt  3872  sbcrext  3873  csbiebt  3928  riota5f  7416  axrepndlem1  10632  axrepndlem2  10633  axunnd  10636  axpowndlem2  10638  axpowndlem3  10639  axpowndlem4  10640  axregndlem2  10643  axinfndlem1  10645  axinfnd  10646  axacndlem4  10650  axacndlem5  10651  axacnd  10652  fproddivf  16023  nfan1c  35087  wl-sbcom2d-lem1  37560  wl-mo2df  37571  wl-eudf  37573  wl-mo3t  37577  wl-ax11-lem4  37589  wl-ax11-lem6  37591
  Copyright terms: Public domain W3C validator