MPE Home 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