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

Theorem nfan1 2202
 Description: A closed form of nfan 1901. (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 400 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2 nfim1.1 . . . 4 𝑥𝜑
3 nfim1.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1859 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfim1 2201 . . 3 𝑥(𝜑 → ¬ 𝜓)
65nfn 1858 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
71, 6nfxfr 1854 1 𝑥(𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  Ⅎ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 1912  ax-6 1971  ax-7 2016  ax-12 2179 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786 This theorem is referenced by:  sb4b  2501  sb4bOLD  2502  ralcom2  3354  sbcralt  3838  sbcrext  3839  csbiebt  3894  riota5f  7124  axrepndlem1  9999  axrepndlem2  10000  axunnd  10003  axpowndlem2  10005  axpowndlem3  10006  axpowndlem4  10007  axregndlem2  10010  axinfndlem1  10012  axinfnd  10013  axacndlem4  10017  axacndlem5  10018  axacnd  10019  fproddivf  15330  wl-sbcom2d-lem1  34860  wl-mo2df  34871  wl-eudf  34873  wl-mo3t  34877  wl-ax11-lem4  34885  wl-ax11-lem6  34887
 Copyright terms: Public domain W3C validator