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

Theorem nfan1 2198
Description: A closed form of nfan 1897. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1781 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 1856 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfim1 2197 . . 3 𝑥(𝜑 → ¬ 𝜓)
65nfn 1855 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
71, 6nfxfr 1850 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781
This theorem is referenced by:  sb4b  2478  ralcom2  3375  sbcralt  3881  sbcrext  3882  csbiebt  3938  riota5f  7416  axrepndlem1  10630  axrepndlem2  10631  axunnd  10634  axpowndlem2  10636  axpowndlem3  10637  axpowndlem4  10638  axregndlem2  10641  axinfndlem1  10643  axinfnd  10644  axacndlem4  10648  axacndlem5  10649  axacnd  10650  fproddivf  16020  nfan1c  35066  wl-sbcom2d-lem1  37540  wl-mo2df  37551  wl-eudf  37553  wl-mo3t  37557  wl-ax11-lem4  37569  wl-ax11-lem6  37571
  Copyright terms: Public domain W3C validator